defpred S₁[ set , set , set ] means ( $2 is Field implies ex K2, K3 being Field st
( K2 = $2 & K3 = $3 & P₁[$1,K2,K3] ) );
A2: 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]
thus ex y being set st S₁[n,x,y] :: thesis: verum

proof

per cases ( not x is Field or x is Field ) ;

suppose B0: x is not Field ; :: thesis: ex y being set st S₁[n,x,y]

take y = 0 ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] by B0; :: thesis: verum

end;

suppose x is Field ; :: thesis: ex y being set st S₁[n,x,y]

then reconsider K2 = x as Field ;
consider K3 being Field such that
B1: P₁[n,K2,K3] by A1;
take y = K3; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] by B1; :: thesis: verum

end;

end;

end;

end;

consider f being Function such that
A3: ( dom f = NAT & f . 0 = F₁() & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 1(A2);
reconsider f = f as sequence by A3, ds;
A4: for i being Nat holds f . i is Field

proof

let i be Nat; :: thesis: f . i is Field
defpred S₂[ Nat] means f . $1 is Field;
IA: S₂[ 0 ] by A3;

IS: now :: thesis: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume IV: S₂[k] ; :: thesis: S₂[k + 1]
S₁[k,f . k,f . (k + 1)] by A3;
hence S₂[k + 1] by IV; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(IA, IS);
hence f . i is Field ; :: thesis: verum

end;

now :: thesis: for x being object st x in rng f holds
x is Field

let x be object ; :: thesis: ( x in rng f implies x is Field )
assume x in rng f ; :: thesis: x is Field
then consider i being object such that
C1: ( i in dom f & f . i = x ) by FUNCT_1:def 3;
reconsider i = i as Element of NAT by C1;
thus x is Field by C1, A4; :: thesis: verum

end;

then reconsider f = f as Field-yielding sequence by defFy;
take f ; :: thesis: ( f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) )
thus f . 0 = F₁() by A3; :: thesis: for n being Nat holds P₁[n,f . n,f . (n + 1)]
thus for n being Nat holds P₁[n,f . n,f . (n + 1)] :: thesis: verum

proof

let n be Nat; :: thesis: P₁[n,f . n,f . (n + 1)]
S₁[n,f . n,f . (n + 1)] by A3;
hence P₁[n,f . n,f . (n + 1)] ; :: thesis: verum

end;