set X = REAL * ;

defpred S_{1}[ object , object ] means for h being Element of REAL * st $1 = h holds

$2 = ((repeat f) . (LifeSpan (f,h,n))) . h;

A1: ex ff being Function st

( f = ff & dom ff = REAL * & rng ff c= REAL * ) by FUNCT_2:def 2;

A3: ( dom f9 = dom f & ( for xx being object st xx in dom f holds

S_{1}[xx,f9 . xx] ) )
from CLASSES1:sch 1(A2);

rng f9 c= REAL *

take f9 ; :: thesis: ( dom f9 = REAL * & ( for h being Element of REAL * holds f9 . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) )

thus dom f9 = REAL * by A1, A3; :: thesis: for h being Element of REAL * holds f9 . h = ((repeat f) . (LifeSpan (f,h,n))) . h

let h be Element of REAL * ; :: thesis: f9 . h = ((repeat f) . (LifeSpan (f,h,n))) . h

thus f9 . h = ((repeat f) . (LifeSpan (f,h,n))) . h by A1, A3; :: thesis: verum

defpred S

$2 = ((repeat f) . (LifeSpan (f,h,n))) . h;

A1: ex ff being Function st

( f = ff & dom ff = REAL * & rng ff c= REAL * ) by FUNCT_2:def 2;

A2: now :: thesis: for xx being object st xx in dom f holds

ex y1 being object st S_{1}[xx,y1]

consider f9 being Function such that ex y1 being object st S

let xx be object ; :: thesis: ( xx in dom f implies ex y1 being object st S_{1}[xx,y1] )

assume xx in dom f ; :: thesis: ex y1 being object st S_{1}[xx,y1]

then reconsider h9 = xx as Element of REAL * by A1;

_{1}[xx,y1]
; :: thesis: verum

end;assume xx in dom f ; :: thesis: ex y1 being object st S

then reconsider h9 = xx as Element of REAL * by A1;

now :: thesis: ex yy being Element of REAL * st

for h being Element of REAL * st xx = h holds

yy = ((repeat f) . (LifeSpan (f,h,n))) . h

hence
ex y1 being object st Sfor h being Element of REAL * st xx = h holds

yy = ((repeat f) . (LifeSpan (f,h,n))) . h

take yy = ((repeat f) . (LifeSpan (f,h9,n))) . h9; :: thesis: for h being Element of REAL * st xx = h holds

yy = ((repeat f) . (LifeSpan (f,h,n))) . h

let h be Element of REAL * ; :: thesis: ( xx = h implies yy = ((repeat f) . (LifeSpan (f,h,n))) . h )

assume xx = h ; :: thesis: yy = ((repeat f) . (LifeSpan (f,h,n))) . h

hence yy = ((repeat f) . (LifeSpan (f,h,n))) . h ; :: thesis: verum

end;yy = ((repeat f) . (LifeSpan (f,h,n))) . h

let h be Element of REAL * ; :: thesis: ( xx = h implies yy = ((repeat f) . (LifeSpan (f,h,n))) . h )

assume xx = h ; :: thesis: yy = ((repeat f) . (LifeSpan (f,h,n))) . h

hence yy = ((repeat f) . (LifeSpan (f,h,n))) . h ; :: thesis: verum

A3: ( dom f9 = dom f & ( for xx being object st xx in dom f holds

S

rng f9 c= REAL *

proof

then reconsider f9 = f9 as Element of Funcs ((REAL *),(REAL *)) by A1, A3, FUNCT_2:def 2;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f9 or y in REAL * )

assume y in rng f9 ; :: thesis: y in REAL *

then consider xx being object such that

A4: xx in dom f9 and

A5: y = f9 . xx by FUNCT_1:def 3;

reconsider h9 = xx as Element of REAL * by A1, A3, A4;

y = ((repeat f) . (LifeSpan (f,h9,n))) . h9 by A3, A4, A5;

hence y in REAL * ; :: thesis: verum

end;assume y in rng f9 ; :: thesis: y in REAL *

then consider xx being object such that

A4: xx in dom f9 and

A5: y = f9 . xx by FUNCT_1:def 3;

reconsider h9 = xx as Element of REAL * by A1, A3, A4;

y = ((repeat f) . (LifeSpan (f,h9,n))) . h9 by A3, A4, A5;

hence y in REAL * ; :: thesis: verum

take f9 ; :: thesis: ( dom f9 = REAL * & ( for h being Element of REAL * holds f9 . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) )

thus dom f9 = REAL * by A1, A3; :: thesis: for h being Element of REAL * holds f9 . h = ((repeat f) . (LifeSpan (f,h,n))) . h

let h be Element of REAL * ; :: thesis: f9 . h = ((repeat f) . (LifeSpan (f,h,n))) . h

thus f9 . h = ((repeat f) . (LifeSpan (f,h,n))) . h by A1, A3; :: thesis: verum