environ
 vocabularies ARYTM, ARYTM_1, RELAT_1, ARYTM_3, FUNCT_1, ABSVALUE, SEQ_4,
   SEQ_2;
 notations SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, COMPLEX1, FUNCT_1,
   RELSET_1, FUNCT_2, SEQ_4, XXREAL_0, PARTFUN3;
 constructors PARTFUN1, XXREAL_0, REAL_1, COMPLEX1, PARTFUN3;
 registrations RELSET_1, XREAL_0, MEMBERED, SEQ_1, RELAT_1, FUNCT_2;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
 definitions SEQ_4;
 theorems XREAL_1, COMPLEX1, SEQ_1, SEQ_4, FUNCT_1, FUNCT_2, XCMPLX_1,
   ABSVALUE;
   
begin
  
reserve
  x,y,z for Element of REAL,
  f,g for Function of REAL,REAL;
  
Lm1: abs(f.x) in rng abs f
     proof
       dom abs f = REAL by FUNCT_2:def 1;
       then (abs f).x = abs(f.x) by SEQ_1:def 10;
       hence abs(f.x) in rng abs f by FUNCT_2:6;
     end;
     
theorem
  (for x,y holds f.(x+y)+f.(x-y)=2*f.x*g.y) &
  (ex x st f.x<>0) & (for x holds abs(f.x)<=1)
  implies for x holds abs(g.x)<=1
  proof
    assume that
A1: for x,y holds f.(x+y)+f.(x-y)=2*f.x*g.y;
    given z such that
A2: f.z<>0;
    assume
A3: for x being Element of REAL holds abs(f.x)<=1;
    let y such that
A4: abs(g.y) > 1;
    set X = rng abs f, k = upper_bound X, D = abs(g.y);
A5: abs(g.y) > 0 by A4,XREAL_1:2;
A6: X is bounded_above
    proof
      take 1;
      let r be real number;
      assume r in X;
      then consider x being set such that
A7:   x in dom abs f and
A8:   (abs f).x = r by FUNCT_1:def 5;
      abs(f.x) = r by A7,A8,SEQ_1:def 10;
      hence r<=1 by A3,A7;
    end;
A9: for s being real number st s in X holds s<=k/D
    proof
      let s be real number;
      assume s in X;
      then consider x being set such that
B1:   x in dom abs f and
B2:   s = (abs f).x by FUNCT_1:def 5;
B3:   s = abs(f.x) by B1,B2,SEQ_1:def 10;
      reconsider x as Element of REAL by B1;
      set A = f.(x+y), B = f.(x-y), C = abs(f.x);
B4:   abs(A+B)<=abs(A)+abs(B) by COMPLEX1:142;
      abs(A) in X & abs(B) in X by Lm1;
      then abs(A)<=k & abs(B)<=k by A6,SEQ_4:def 4;
      then
B5:   abs(A)+abs(B)<=k+k by XREAL_1:9;
      abs(A+B) = abs(2*f.x*g.y) by A1
      .= abs(2*f.x)*D by COMPLEX1:151
      .= abs(2)*C*D by COMPLEX1:151
      .= 2*C*D by ABSVALUE:def 1;
      then 2*(C*D)<=2*k by B4,B5,XREAL_1:2;
      then C*D<=k by XREAL_1:70;
      then C*D/D<=k/D by A5,XREAL_1:74;
      hence thesis by A5,B3,XCMPLX_1:90;
    end;
    abs(f.z) in X by Lm1;
    then
B6: abs(f.z)<=k by A6,SEQ_4:def 4;
    0<abs(f.z) by A2,COMPLEX1:133;
    then 0<k by B6,XREAL_1:2;
    then k/D<k/1 by A4,XREAL_1:78;
    hence thesis by A9,SEQ_4:62;
  end;