let X, Y be set ; :: thesis: for F, G being Function of NAT,(bool X) st ( for i being Nat holds G . i = (F . i) /\ Y ) & Union F = Y holds
Union G = Union F
let F, G be Function of NAT,(bool X); :: thesis: ( ( for i being Nat holds G . i = (F . i) /\ Y ) & Union F = Y implies Union G = Union F )
assume that
A1: for i being Nat holds G . i = (F . i) /\ Y and
A2: Union F = Y ; :: thesis: Union G = Union F

now :: thesis: for x being object st x in Union G holds
x in Union F

let x be object ; :: thesis: ( x in Union G implies x in Union F )
assume x in Union G ; :: thesis: x in Union F
then x in union (rng G) by CARD_3:def 4;
then consider A being set such that
A3: ( x in A & A in rng G ) by TARSKI:def 4;
consider i being Element of NAT such that
A4: A = G . i by A3, FUNCT_2:113;
dom F = NAT by FUNCT_2:def 1;
then ( A = (F . i) /\ Y & i in dom F ) by A1, A4;
then ( x in F . i & F . i in rng F ) by A3, XBOOLE_0:def 4, FUNCT_1:3;
then x in union (rng F) by TARSKI:def 4;
hence x in Union F by CARD_3:def 4; :: thesis: verum

end;

then A5: Union G c= Union F by TARSKI:def 3;

now :: thesis: for x being object st x in Union F holds
x in Union G

let x be object ; :: thesis: ( x in Union F implies x in Union G )
assume A6: x in Union F ; :: thesis: x in Union G
then x in union (rng F) by CARD_3:def 4;
then consider A being set such that
A7: ( x in A & A in rng F ) by TARSKI:def 4;
consider i being Element of NAT such that
A8: A = F . i by A7, FUNCT_2:113;
dom G = NAT by FUNCT_2:def 1;
then ( x in (F . i) /\ Y & i in dom G ) by A2, A6, A7, A8, XBOOLE_0:def 4;
then ( x in G . i & G . i in rng G ) by A1, FUNCT_1:3;
then x in union (rng G) by TARSKI:def 4;
hence x in Union G by CARD_3:def 4; :: thesis: verum

end;

then Union F c= Union G by TARSKI:def 3;
hence Union G = Union F by A5, XBOOLE_0:def 10; :: thesis: verum