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

let n be Element of NAT ; :: thesis:
A4: ( n = 0 implies H . n c= F . n ) by A2;
( ex k being Nat st n = k + 1 implies H . n c= F . n )

given k being Nat such that A5: n = k + 1 ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 13;
H . n = (F . n) \ (G . k) by A2, A5;
hence H . n c= F . n ; :: thesis:

end;

hence H . n c= F . n by A4, NAT_1:6; :: thesis:

end;

A6: union (rng H) c= union (rng F)

let r be set ; :: according to TARSKI:def 3 :: thesis:
assume r in union (rng H) ; :: thesis:
then consider E being set such that
A7: ( r in E & E in rng H ) by TARSKI:def 4;
consider s being set such that
A8: ( s in dom H & E = H . s ) by A7, FUNCT_1:def 5;
reconsider s = s as Element of NAT by A8;
A9: E c= F . s by A3, A8;
F . s in rng F by FUNCT_2:6;
hence r in union (rng F) by A7, A9, TARSKI:def 4; :: thesis:

end;

thus union (rng F) c= union (rng H) :: according to XBOOLE_0:def 10 :: thesis:

let r be set ; :: according to TARSKI:def 3 :: thesis:
assume r in union (rng F) ; :: thesis:
then consider E being set such that
A10: ( r in E & E in rng F ) by TARSKI:def 4;
consider s being set such that
A11: ( s in dom F & E = F . s ) by A10, FUNCT_1:def 5;
ex s1 being Element of NAT st r in H . s1

defpred S₁[ Nat] means r in F . $1;
A12: ex k being Nat st S₁[k] by A10, A11;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A12);
then consider k being Nat such that
A13: ( r in F . k & ( for n being Nat st r in F . n holds
k <= n ) ) ;
A14: ( k = 0 implies ex s1 being Element of NAT st r in H . s1 ) by A2, A13;
( ex l being Nat st k = l + 1 implies ex s1 being Element of NAT st r in H . s1 )

given l being Nat such that A15: k = l + 1 ; :: thesis:
reconsider l = l as Element of NAT by ORDINAL1:def 13;
A16: not r in G . l

assume r in G . l ; :: thesis:
then consider i being Element of NAT such that
A17: ( i <= l & r in F . i ) by A1, MEASURE2:6;
k <= i by A13, A17;
hence contradiction by A15, A17, NAT_1:13; :: thesis:

end;

A18: H . (l + 1) = (F . (l + 1)) \ (G . l) by A2;
take k ; :: thesis:
thus ( k is Element of REAL & k is Element of NAT & r in H . k ) by A13, A15, A16, A18, XBOOLE_0:def 5; :: thesis:

end;

hence ex s1 being Element of NAT st r in H . s1 by A14, NAT_1:6; :: thesis:

end;

then consider s1 being Element of NAT such that
A19: r in H . s1 ;
H . s1 in rng H by FUNCT_2:6;
hence r in union (rng H) by A19, TARSKI:def 4; :: thesis:

end;

thus union (rng H) c= union (rng F) by A6; :: thesis: