let X, Y, a be set ; :: thesis: ( X c= Y implies X --> a c= Y --> a )
A1: dom (X --> a) = X by FUNCOP_1:19;
assume A2: X c= Y ; :: thesis: X --> a c= Y --> a

A3: now

let x be set ; :: 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:13;
hence (X --> a) . x = (Y --> a) . x by A2, A1, A4, FUNCOP_1:13; :: thesis: verum

end;

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