let x be set ; :: thesis: for f, g being Function st rng f c= rng g & x in dom f holds
ex y being object st
( y in dom g & f . x = g . y )
let f, g be Function; :: thesis: ( rng f c= rng g & x in dom f implies ex y being object st
( y in dom g & f . x = g . y ) )
assume that
A1: rng f c= rng g and
A2: x in dom f ; :: thesis: ex y being object st
( y in dom g & f . x = g . y )
f . x in rng f by A2, FUNCT_1:3;
hence ex y being object st
( y in dom g & f . x = g . y ) by A1, FUNCT_1:def 3; :: thesis: verum