let f, g be Function; :: thesis: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) implies rng f c= rng g )
assume that
A2: dom f c= dom g and
A2a: for x being set st x in dom f holds
f . x = g . x ; :: thesis: rng f c= rng g
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in rng g )
assume x in rng f ; :: thesis: x in rng g
then consider y being object such that
A1: ( y in dom f & x = f . y ) by FUNCT_1:def 3;
x = g . y by A2a, A1;
hence x in rng g by FUNCT_1:3, A1, A2; :: thesis: verum