let X be set ; :: thesis: for S being non empty Subset-Family of X
for N, F being Function of NAT ,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for n, m being Element of NAT st n < m holds
F . n c= F . m
let S be non empty Subset-Family of X; :: thesis: for N, F being Function of NAT ,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for n, m being Element of NAT st n < m holds
F . n c= F . m
let N, F be Function of NAT ,S; :: thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) implies for n, m being Element of NAT st n < m holds
F . n c= F . m )
assume that
A1: F . 0 = N . 0 and
A2: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; :: thesis: for n, m being Element of NAT st n < m holds
F . n c= F . m
defpred S1[ Element of NAT ] means for m being Element of NAT st $1 < m holds
F . $1 c= F . m;
A3: S1[ 0 ]
proof
A4: for k being Element of NAT st 0 < k + 1 holds
F . 0 c= F . (k + 1)
proof
defpred S2[ Element of NAT ] means ( 0 < $1 + 1 implies F . 0 c= F . ($1 + 1) );
A5: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of 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 Element of NAT holds S2[k] from NAT_1:sch 1(A8, A5); :: thesis: verum
end;
let m be Element of 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 13;
m = k + 1 by A10;
hence F . 0 c= F . m by A9, A4; :: thesis: verum
end;
A11: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A12: for m being Element of NAT st n < m holds
F . n c= F . m ; :: thesis: S1[n + 1]
let m be Element of 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 set ; :: 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, Th6;
hence r in F . m by A16, A17, A14, XBOOLE_0:def 3; :: thesis: verum
end;
thus for n being Element of NAT holds S1[n] from NAT_1:sch 1(A3, A11); :: thesis: verum