let f, g be Function; :: thesis: ( f c= g implies Union f c= Union g )
assume f c= g ; :: thesis: Union f c= Union g
then A1: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) by GRFUNC_1:8;
let x be set ; :: 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
A2: ( x in X & X in rng f ) by TARSKI:def 4;
consider y being set such that
A3: ( y in dom f & X = f . y ) by A2, FUNCT_1:def 5;
( y in dom g & f . y = g . y ) by A1, A3;
then X in rng g by A3, FUNCT_1:def 5;
hence x in Union g by A2, TARSKI:def 4; :: thesis: verum