set X = REAL * ;
defpred S1[ 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;
A2: now :: thesis: for xx being object st xx in dom f holds
ex y1 being object st S1[xx,y1]
let xx be object ; :: thesis: ( xx in dom f implies ex y1 being object st S1[xx,y1] )
assume xx in dom f ; :: thesis: ex y1 being object st S1[xx,y1]
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
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;
hence ex y1 being object st S1[xx,y1] ; :: thesis: verum
end;
consider f9 being Function such that
A3: ( dom f9 = dom f & ( for xx being object st xx in dom f holds
S1[xx,f9 . xx] ) ) from CLASSES1:sch 1(A2);
 rng f9 c= REAL *
proof
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;
then reconsider f9 = f9 as Element of Funcs ((REAL *),(REAL *)) by A1, A3, FUNCT_2:def 2;
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