let V be ManySortedSet of ; :: 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;

B2: now

let j be Element of NAT ; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume S₁[j] ; :: thesis: S₁[j + 1]
B3: 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 set ; :: 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 ( ex i being Element of NAT st x = [{} ,i] & {} c= V . j ) by A1, XBOOLE_1:2;
hence x in V . (j + 1) by B3, Th11; :: thesis: verum

end;

end;

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

A5: now

let j be Element of NAT ; :: thesis: ( S₂[j] implies S₂[j + 1] )
assume B4: S₂[j] ; :: thesis: S₂[j + 1]
B5: 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 B2; :: 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
B6: j = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
B7: V . j = { [(varcl A),n] where A is Subset of (V . k), n is Element of NAT : A is finite } by A2, B6;
B8: V . (j + 1) = { [(varcl A),n] where A is Subset of (V . j), n is Element of NAT : A is finite } by A2;
B9: V . k c= V . j by B4, B6, NAT_1:11;
let x be set ; :: 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
C1: ( x = [(varcl A),n] & A is finite ) by B7;
A c= V . j by B9, XBOOLE_1:1;
hence x in V . (j + 1) by B8, C1; :: 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 B4, NAT_1:8;
hence V . i c= V . (j + 1) by B5, XBOOLE_1:1; :: thesis: verum

end;

end;

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