let X be set ; :: thesis: for S being non empty Subset-Family of X
for N, G, F being Function of NAT ,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n <= m holds
F . n c= G . m
let S be non empty Subset-Family of X; :: thesis: for N, G, F being Function of NAT ,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Element of NAT st n <= m holds
F . n c= G . m
let N, G, F be Function of NAT ,S; :: thesis: ( G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) implies for n, m being Element of NAT st n <= m holds
F . n c= G . m )
assume A1: ( G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) ) ; :: thesis: for n, m being Element of NAT st n <= m holds
F . n c= G . m
A2: for n being Element of NAT holds F . n c= G . n

proof

defpred S₁[ Element of NAT ] means F . $1 c= G . $1;
A3: S₁[ 0 ] by A1;
A4: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume F . n c= G . n ; :: thesis: S₁[n + 1]
A5: F . (n + 1) = (N . (n + 1)) \ (G . n) by A1;
G . (n + 1) = (N . (n + 1)) \/ (G . n) by A1;
then N . (n + 1) c= G . (n + 1) by XBOOLE_1:7;
hence S₁[n + 1] by A5, XBOOLE_1:1; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4); :: thesis: verum

end;

let n, m be Element of NAT ; :: thesis: ( n <= m implies F . n c= G . m )
assume n <= m ; :: thesis: F . n c= G . m
then A6: ( n = m or n < m ) by XXREAL_0:1;
( n < m implies F . n c= G . m )

proof

assume A7: n < m ; :: thesis: F . n c= G . m
A8: F . n c= G . n by A2;
G . n c= G . m by A1, A7, Th7;
hence F . n c= G . m by A8, XBOOLE_1:1; :: thesis: verum

end;

hence F . n c= G . m by A2, A6; :: thesis: verum