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

now

let x be set ; :: thesis: ( x in dom (X --> a) implies (X --> a) . x = (Y --> a) . x )
assume x in dom (X --> a) ; :: thesis: (X --> a) . x = (Y --> a) . x
then ( (X --> a) . x = a & (Y --> a) . x = a ) by A1, A2, FUNCOP_1:13;
hence (X --> a) . x = (Y --> a) . x ; :: thesis: verum

end;

hence X --> a c= Y --> a by A1, A2, GRFUNC_1:8; :: thesis: verum