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;