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

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