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 that
A1: G . 0 = N . 0 and
A2: for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) and
A3: F . 0 = N . 0 and
A4: 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
let n, m be Element of NAT ; :: thesis: ( n <= m implies F . n c= G . m )
A5: for n being Element of NAT holds F . n c= G . n

proof

defpred S₁[ Element of NAT ] means F . $1 c= G . $1;
A6: 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]
G . (n + 1) = (N . (n + 1)) \/ (G . n) by A2;
then A7: N . (n + 1) c= G . (n + 1) by XBOOLE_1:7;
F . (n + 1) = (N . (n + 1)) \ (G . n) by A4;
hence S₁[n + 1] by A7, XBOOLE_1:1; :: thesis: verum

end;

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

end;

A9: ( n < m implies F . n c= G . m )

proof

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

end;

assume n <= m ; :: thesis: F . n c= G . m
then ( n = m or n < m ) by XXREAL_0:1;
hence F . n c= G . m by A5, A9; :: thesis: verum