set X = REAL * ;
defpred S₁[ set , set ] 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

let xx be set ; :: thesis: ( xx in dom f implies ex y1 being set st S₁[xx,y1] )
assume xx in dom f ; :: thesis: ex y1 being set st S₁[xx,y1]
then reconsider h' = xx as Element of REAL * by A1;

now

take yy = ((repeat f) . (LifeSpan f,h',n)) . h'; :: 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 set st S₁[xx,y1] ; :: thesis: verum

end;

consider f' being Function such that
A3: ( dom f' = dom f & ( for xx being set st xx in dom f holds
S₁[xx,f' . xx] ) ) from CLASSES1:sch 1(A2);
rng f' c= REAL *

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f' or y in REAL * )
assume y in rng f' ; :: thesis: y in REAL *
then consider xx being set such that
A4: xx in dom f' and
A5: y = f' . xx by FUNCT_1:def 5;
reconsider h' = xx as Element of REAL * by A1, A3, A4;
y = ((repeat f) . (LifeSpan f,h',n)) . h' by A3, A4, A5;
hence y in REAL * ; :: thesis: verum

end;

then reconsider f' = f' as Element of Funcs (REAL * ),(REAL * ) by A1, A3, FUNCT_2:def 2;
take f' ; :: thesis: ( dom f' = REAL * & ( for h being Element of REAL * holds f' . h = ((repeat f) . (LifeSpan f,h,n)) . h ) )
thus dom f' = REAL * by A1, A3; :: thesis: for h being Element of REAL * holds f' . h = ((repeat f) . (LifeSpan f,h,n)) . h
let h be Element of REAL * ; :: thesis: f' . h = ((repeat f) . (LifeSpan f,h,n)) . h
thus f' . h = ((repeat f) . (LifeSpan f,h,n)) . h by A1, A3; :: thesis: verum