let V be ManySortedSet of NAT ; :: thesis: ( V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) implies for i, j being Element of NAT st i <= j holds
V . i c= V . j )
assume that
A1: V . 0 = { [{},i] where i is Element of NAT : verum } and
A2: for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ; :: thesis: for i, j being Element of NAT st i <= j holds
V . i c= V . j
defpred S₁[ Nat] means V . 0 c= V . $1;

A3: now :: thesis: for j being Element of NAT st S₁[j] holds
S₁[j + 1]

let j be Element of NAT ; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume S₁[j] ; :: thesis: S₁[j + 1]
A4: V . (j + 1) = { [(varcl A),k] where A is Subset of (V . j), k is Element of NAT : A is finite } by A2;
thus S₁[j + 1] :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V . 0 or x in V . (j + 1) )
assume x in V . 0 ; :: thesis: x in V . (j + 1)
then A5: ex i being Element of NAT st x = [{},i] by A1;
{} c= V . j ;
hence x in V . (j + 1) by A4, A5, Th8; :: thesis: verum

end;

end;

defpred S₂[ Nat] means for i being Nat st i <= $1 holds
V . i c= V . $1;
A6: S₂[ 0 ] by NAT_1:3;

A7: now :: thesis: for j being Nat st S₂[j] holds
S₂[j + 1]

let j be Nat; :: thesis: ( S₂[j] implies S₂[j + 1] )
assume A8: S₂[j] ; :: thesis: S₂[j + 1]
A9: V . j c= V . (j + 1)

proof

per cases ( j = 0 or ex k being Nat st j = k + 1 ) by NAT_1:6;

suppose j = 0 ; :: thesis: V . j c= V . (j + 1)

hence V . j c= V . (j + 1) by A3; :: thesis: verum

end;

suppose ex k being Nat st j = k + 1 ; :: thesis: V . j c= V . (j + 1)

then consider k being Nat such that
A10: j = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A11: V . j = { [(varcl A),n] where A is Subset of (V . k), n is Element of NAT : A is finite } by A2, A10;
A12: V . (j + 1) = { [(varcl A),n] where A is Subset of (V . j), n is Element of NAT : A is finite } by A2;
A13: V . k c= V . j by A8, A10, NAT_1:11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V . j or x in V . (j + 1) )
assume x in V . j ; :: thesis: x in V . (j + 1)
then consider A being Subset of (V . k), n being Element of NAT such that
A14: x = [(varcl A),n] and
A15: A is finite by A11;
A c= V . j by A13;
hence x in V . (j + 1) by A12, A14, A15; :: thesis: verum

end;

end;

end;

thus S₂[j + 1] :: thesis: verum

proof

let i be Nat; :: thesis: ( i <= j + 1 implies V . i c= V . (j + 1) )
assume i <= j + 1 ; :: thesis: V . i c= V . (j + 1)
then ( i = j + 1 or V . i c= V . j ) by A8, NAT_1:8;
hence V . i c= V . (j + 1) by A9; :: thesis: verum

end;

end;

for j being Nat holds S₂[j] from NAT_1:sch 2(A6, A7);
hence for i, j being Element of NAT st i <= j holds
V . i c= V . j ; :: thesis: verum