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 that
A1: G . 0 = F . 0 and
A2: 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 that
A3: H . 0 = F . 0 and
A4: for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ; :: thesis:
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
A5: r in E and
A6: E in rng F by TARSKI:def 4;
A7: ex s being set st
( s in dom F & E = F . s ) by A6, FUNCT_1:def 5;
ex s1 being Element of NAT st r in H . s1

defpred S₁[ Nat] means r in F . $1;
A8: ex k being Nat st S₁[k] by A5, A7;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A8);
then consider k being Nat such that
A9: r in F . k and
A10: for n being Nat st r in F . n holds
k <= n ;
A11: ( 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 A12: k = l + 1 ; :: thesis:
take k ; :: thesis:
reconsider l = l as Element of NAT by ORDINAL1:def 13;
A13: not r in G . l

assume r in G . l ; :: thesis:
then consider i being Element of NAT such that
A14: i <= l and
A15: r in F . i by A1, A2, MEASURE2:6;
k <= i by A10, A15;
hence contradiction by A12, A14, NAT_1:13; :: thesis:

end;

H . (l + 1) = (F . (l + 1)) \ (G . l) by A4;
hence ( k is Element of REAL & k is Element of NAT & r in H . k ) by A9, A12, A13, XBOOLE_0:def 5; :: thesis:

end;

( k = 0 implies ex s1 being Element of NAT st r in H . s1 ) by A3, A9;
hence ex s1 being Element of NAT st r in H . s1 by A11, NAT_1:6; :: thesis:

end;

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

end;

A17: for n being Element of NAT holds H . n c= F . n

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

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

end;

( n = 0 implies H . n c= F . n ) by A3;
hence H . n c= F . n by A18, NAT_1:6; :: thesis:

end;

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
A20: r in E and
A21: E in rng H by TARSKI:def 4;
consider s being set such that
A22: s in dom H and
A23: E = H . s by A21, FUNCT_1:def 5;
reconsider s = s as Element of NAT by A22;
A24: F . s in rng F by FUNCT_2:6;
E c= F . s by A17, A23;
hence r in union (rng F) by A20, A24, TARSKI:def 4; :: thesis:

end;

hence union (rng H) c= union (rng F) ; :: thesis: