let a be object ; :: thesis: for X, Y being set st X c= Y holds
X --> a c= Y --> a
let X, Y be set ; :: thesis: ( X c= Y implies X --> a c= Y --> a )
assume A2: X c= Y ; :: thesis: X --> a c= Y --> a

A3: now :: thesis: for x being object st x in dom (X --> a) holds
(X --> a) . x = (Y --> a) . x

let x be object ; :: thesis: ( x in dom (X --> a) implies (X --> a) . x = (Y --> a) . x )
assume A4: x in dom (X --> a) ; :: thesis: (X --> a) . x = (Y --> a) . x
then (X --> a) . x = a by FUNCOP_1:7;
hence (X --> a) . x = (Y --> a) . x by A2, A4, FUNCOP_1:7; :: thesis: verum

end;

dom (Y --> a) = Y ;
hence X --> a c= Y --> a by A2, A3, GRFUNC_1:2; :: thesis: verum