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