per cases ( [f1,f2] in dom the composition of C or Mor C is empty ) by A1;

suppose [f1,f2] in dom the composition of C ; :: thesis: the composition of C . (f1,f2) is morphism of C

then the composition of C . [f1,f2] in rng the composition of C by FUNCT_1:3;
hence the composition of C . (f1,f2) is morphism of C by BINOP_1:def 1; :: thesis: verum

end;

suppose A2: Mor C is empty ; :: thesis: the composition of C . (f1,f2) is morphism of C

the composition of C . [f1,f2] = the composition of C . (f1,f2) by BINOP_1:def 1;
hence the composition of C . (f1,f2) is morphism of C by A2, SUBSET_1:def 1; :: thesis: verum

end;

end;