let X, Y be non empty set ; :: thesis: for E being set
for F, G being Function of X,Y st ( for x being Element of X holds G . x = E \ (F . x) ) holds
union (rng G) = E \ (meet (rng F))
let E be set ; :: thesis: for F, G being Function of X,Y st ( for x being Element of X holds G . x = E \ (F . x) ) holds
union (rng G) = E \ (meet (rng F))
let F, G be Function of X,Y; :: thesis: ( ( for x being Element of X holds G . x = E \ (F . x) ) implies union (rng G) = E \ (meet (rng F)) )
assume A1: for x being Element of X holds G . x = E \ (F . x) ; :: thesis: union (rng G) = E \ (meet (rng F))
A2: ( dom F = X & dom G = X ) by FUNCT_2:def 1;

now

let Z be set ; :: thesis: ( Z in DIFFERENCE {E},(rng F) implies Z in rng G )
assume Z in DIFFERENCE {E},(rng F) ; :: thesis: Z in rng G
then consider X1, Y being set such that
A3: ( X1 in {E} & Y in rng F & Z = X1 \ Y ) by SETFAM_1:def 6;
consider x being set such that
A4: ( x in dom F & Y = F . x ) by A3, FUNCT_1:def 5;
reconsider x = x as Element of X by A4;
X1 = E by A3, TARSKI:def 1;
then Z = G . x by A1, A3, A4;
hence Z in rng G by A2, FUNCT_1:12; :: thesis: verum

end;

then A5: DIFFERENCE {E},(rng F) c= rng G by TARSKI:def 3;

now

let Z be set ; :: thesis: ( Z in rng G implies Z in DIFFERENCE {E},(rng F) )
assume Z in rng G ; :: thesis: Z in DIFFERENCE {E},(rng F)
then consider x being set such that
A6: ( x in dom G & Z = G . x ) by FUNCT_1:def 5;
reconsider x = x as Element of X by A6;
A7: Z = E \ (F . x) by A1, A6;
A8: F . x in rng F by A2, FUNCT_1:12;
E in {E} by TARSKI:def 1;
hence Z in DIFFERENCE {E},(rng F) by A7, A8, SETFAM_1:def 6; :: thesis: verum

end;

then rng G c= DIFFERENCE {E},(rng F) by TARSKI:def 3;
then DIFFERENCE {E},(rng F) = rng G by A5, XBOOLE_0:def 10;
hence union (rng G) = E \ (meet (rng F)) by SETFAM_1:38; :: thesis: verum