let f, g be Function; :: thesis: ( f c= g iff for x being set st x in dom f holds
( x in dom g & f . x = g . x ) )
defpred S₁[] means for x being object st x in dom f holds
x in dom g;
defpred S₂[] means for x being object st x in dom f holds
f . x = g . x;
( S₁[] & S₂[] iff ( dom f c= dom g & S₂[] ) ) ;
hence ( f c= g iff for x being set st x in dom f holds
( x in dom g & f . x = g . x ) ) by GRFUNC_1:2; :: thesis: verum