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 S1[ Nat] means V . 0 c= V . $1;
A3: now :: thesis: for j being Element of NAT st S1[j] holds
S1[j + 1]
let j be Element of NAT ; :: thesis: ( S1[j] implies S1[j + 1] )
assume S1[j] ; :: thesis: S1[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 S1[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 S2[ Nat] means for i being Nat st i <= $1 holds
V . i c= V . $1;
A6: S2[ 0 ] by NAT_1:3;
A7: now :: thesis: for j being Nat st S2[j] holds
S2[j + 1]
let j be Nat; :: thesis: ( S2[j] implies S2[j + 1] )
assume A8: S2[j] ; :: thesis: S2[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 S2[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 S2[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