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 G = X by FUNCT_2:def 1;

now :: thesis: for Z being object st Z in DIFFERENCE ({E},(rng F)) holds
Z in rng G

let Z be object ; :: 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} and
A4: Y in rng F and
A5: Z = X1 \ Y by SETFAM_1:def 6;
consider x being object such that
A6: x in dom F and
A7: Y = F . x by A4, FUNCT_1:def 3;
reconsider x = x as Element of X by A6;
X1 = E by A3, TARSKI:def 1;
then Z = G . x by A1, A5, A7;
hence Z in rng G by A2, FUNCT_1:3; :: thesis: verum

end;

then A8: DIFFERENCE ({E},(rng F)) c= rng G ;
A9: dom F = X by FUNCT_2:def 1;

now :: thesis: for Z being object st Z in rng G holds
Z in DIFFERENCE ({E},(rng F))

let Z be object ; :: thesis: ( Z in rng G implies Z in DIFFERENCE ({E},(rng F)) )
A10: E in {E} by TARSKI:def 1;
assume Z in rng G ; :: thesis: Z in DIFFERENCE ({E},(rng F))
then consider x being object such that
A11: x in dom G and
A12: Z = G . x by FUNCT_1:def 3;
reconsider x = x as Element of X by A11;
A13: F . x in rng F by A9, FUNCT_1:3;
Z = E \ (F . x) by A1, A12;
hence Z in DIFFERENCE ({E},(rng F)) by A13, A10, SETFAM_1:def 6; :: thesis: verum

end;

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