defpred S₁[ set , set , set ] means for z being set st z = $2 holds
$3 = F₃($1,z);
A1: for n being Nat
for x being set ex y being set st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being set ex y being set st S₁[n,x,y]
let x be set ; :: thesis: ex y being set st S₁[n,x,y]
take F₃(n,x) ; :: thesis: S₁[n,x,F₃(n,x)]
thus S₁[n,x,F₃(n,x)] ; :: thesis: verum

end;

A2: for n being Nat
for x, y1, y2 being set st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2

proof

let n be Nat; :: thesis: for x, y1, y2 being set st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2
let x, y1, y2 be set ; :: thesis: ( S₁[n,x,y1] & S₁[n,x,y2] implies y1 = y2 )
assume that
A3: for z being set st z = x holds
y1 = F₃(n,z) and
A4: for z being set st z = x holds
y2 = F₃(n,z) ; :: thesis: y1 = y2
thus y1 = F₃(n,x) by A3
.= y2 by A4 ; :: thesis: verum

end;

A5: ( ex y being set ex f being Function st
( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) ) from RECDEF_1:sch 11(A1, A2);
then consider y being set , f being Function such that
A6: ( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) ;
thus ex y being set ex f being Function st
( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) :: thesis: for y1, y2 being set st ex f being Function st
( y1 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) & ex f being Function st
( y2 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) holds
y1 = y2

proof

take y ; :: thesis: ex f being Function st
( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) )
take f ; :: thesis: ( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) )
thus ( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) by A6; :: thesis: verum

end;

let y1, y2 be set ; :: thesis: ( ex f being Function st
( y1 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) & ex f being Function st
( y2 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) implies y1 = y2 )
given f1 being Function such that A7: ( y1 = f1 . F₂() & dom f1 = NAT & f1 . 0 = F₁() ) and
A8: for n being Nat holds f1 . (n + 1) = F₃(n,(f1 . n)) ; :: thesis: ( for f being Function holds
( not y2 = f . F₂() or not dom f = NAT or not f . 0 = F₁() or ex n being Nat st not f . (n + 1) = F₃(n,(f . n)) ) or y1 = y2 )
A9: for n being Nat holds S₁[n,f1 . n,f1 . (n + 1)] by A8;
given f2 being Function such that A10: ( y2 = f2 . F₂() & dom f2 = NAT & f2 . 0 = F₁() ) and
A11: for n being Nat holds f2 . (n + 1) = F₃(n,(f2 . n)) ; :: thesis: y1 = y2
for n being Nat holds S₁[n,f2 . n,f2 . (n + 1)] by A11;
hence y1 = y2 by A5, A7, A10, A9; :: thesis: verum