let X be set ; :: thesis: for S being non empty Subset-Family of X
for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for n, m being Nat st n < m holds
F . n c= F . m
let S be non empty Subset-Family of X; :: thesis: for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for n, m being Nat st n < m holds
F . n c= F . m
let N, F be sequence of S; :: thesis: ( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) implies for n, m being Nat st n < m holds
F . n c= F . m )
assume that
A1: F . 0 = N . 0 and
A2: for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; :: thesis: for n, m being Nat st n < m holds
F . n c= F . m
defpred S1[ Nat] means for m being Nat st $1 < m holds
F . $1 c= F . m;
A3: S1[ 0 ]
proof
A4: for k being Nat st 0 < k + 1 holds
F . 0 c= F . (k + 1)
proof
defpred S2[ Nat] means ( 0 < $1 + 1 implies F . 0 c= F . ($1 + 1) );
A5: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
A6: 0 <= k by NAT_1:2;
F . ((k + 1) + 1) = (N . ((k + 1) + 1)) \/ (F . (k + 1)) by A2;
then A7: F . (k + 1) c= F . ((k + 1) + 1) by XBOOLE_1:7;
assume ( 0 < k + 1 implies F . 0 c= F . (k + 1) ) ; :: thesis: S2[k + 1]
hence S2[k + 1] by A7, A6, NAT_1:13, XBOOLE_1:1; :: thesis: verum
end;
F . (0 + 1) = (N . (0 + 1)) \/ (F . 0) by A2;
then A8: S2[ 0 ] by XBOOLE_1:7;
thus for k being Nat holds S2[k] from NAT_1:sch 2(A8, A5); :: thesis: verum
end;
let m be Nat; :: thesis: ( 0 < m implies F . 0 c= F . m )
assume A9: 0 < m ; :: thesis: F . 0 c= F . m
then consider k being Nat such that
A10: m = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
m = k + 1 by A10;
hence F . 0 c= F . m by A9, A4; :: thesis: verum
end;
A11: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A12: for m being Nat st n < m holds
F . n c= F . m ; :: thesis: S1[n + 1]
let m be Nat; :: thesis: ( n + 1 < m implies F . (n + 1) c= F . m )
assume A13: n + 1 < m ; :: thesis: F . (n + 1) c= F . m
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in F . (n + 1) or r in F . m )
A14: ( r in F . n implies r in F . m )
proof
assume A15: r in F . n ; :: thesis: r in F . m
( n < m implies r in F . m )
proof
assume n < m ; :: thesis: r in F . m
then F . n c= F . m by A12;
hence r in F . m by A15; :: thesis: verum
end;
hence r in F . m by A13, NAT_1:13; :: thesis: verum
end;
assume A16: r in F . (n + 1) ; :: thesis: r in F . m
A17: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2;
( r in N . (n + 1) implies r in F . m ) by A1, A2, A13, Th5;
hence r in F . m by A16, A17, A14, XBOOLE_0:def 3; :: thesis: verum
end;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A3, A11); :: thesis: verum