let f, g be Function; :: thesis: ( f c= g implies Union f c= Union g )
assume A1: f c= g ; :: thesis: Union f c= Union g
then A2: dom f c= dom g by GRFUNC_1:2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union f or x in Union g )
assume x in Union f ; :: thesis: x in Union g
then consider X being set such that
A3: x in X and
A4: X in rng f by TARSKI:def 4;
consider y being object such that
A5: y in dom f and
A6: X = f . y by A4, FUNCT_1:def 3;
f . y = g . y by A1, A5, GRFUNC_1:2;
then X in rng g by A2, A5, A6, FUNCT_1:def 3;
hence x in Union g by A3, TARSKI:def 4; :: thesis: verum