set fg = f * g;
let h be Function; :: according to MATRTOP3:def 1 :: thesis: for x being set st h in dom (f * g) & ((f * g) . h) . x <> h . x holds
x in X \/ Y
let x be set ; :: thesis: ( h in dom (f * g) & ((f * g) . h) . x <> h . x implies x in X \/ Y )
assume that
A2: h in dom (f * g) and
A3: ((f * g) . h) . x <> h . x ; :: thesis: x in X \/ Y
A4: h in dom g by A2, FUNCT_1:11;
assume A5: not x in X \/ Y ; :: thesis: contradiction
then not x in Y by XBOOLE_0:def 3;
then A6: (g . h) . x = h . x by A4, Def1;
A7: ( (f * g) . h = f . (g . h) & g . h in dom f ) by A2, FUNCT_1:11, FUNCT_1:12;
not x in X by A5, XBOOLE_0:def 3;
hence contradiction by A3, A6, A7, Def1; :: thesis: verum