let C be associative composable with_identities CategoryStr ; :: thesis: for f, g, h being Element of Mor C st (SourceMap C) . h = (TargetMap C) . g & (SourceMap C) . g = (TargetMap C) . f holds
(CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)
let f, g, h be Element of Mor C; :: thesis: ( (SourceMap C) . h = (TargetMap C) . g & (SourceMap C) . g = (TargetMap C) . f implies (CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f) )
assume A1: ( (SourceMap C) . h = (TargetMap C) . g & (SourceMap C) . g = (TargetMap C) . f ) ; :: thesis: (CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)
per cases ( C is empty or not C is empty ) ;
suppose A2: C is empty ; :: thesis: (CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)
thus (CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . [h,((CompMap C) . (g,f))] by BINOP_1:def 1
.= {} by A2
.= (CompMap C) . [((CompMap C) . (h,g)),f] by A2
.= (CompMap C) . (((CompMap C) . (h,g)),f) by BINOP_1:def 1 ; :: thesis: verum
end;
suppose A3: not C is empty ; :: thesis: (CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)
A4: [h,g] in dom (CompMap C) by Th37, A3, A1;
then A5: h |> g ;
A6: [g,f] in dom (CompMap C) by Th37, A3, A1;
then A7: g |> f ;
A8: h |> g (*) f by A7, A5, Lm3;
A9: h (*) g |> f by A7, A5, Lm3;
A10: (CompMap C) . (g,f) = the composition of C . [g,f] by BINOP_1:def 1
.= g (*) f by A6, Def2, Lm4 ;
A11: (CompMap C) . (h,g) = the composition of C . [h,g] by BINOP_1:def 1
.= h (*) g by A4, Def2, Lm4 ;
thus (CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . [h,(g (*) f)] by A10, BINOP_1:def 1
.= h (*) (g (*) f) by A8, Lm4
.= (h (*) g) (*) f by A5, A7, Lm5
.= (CompMap C) . [(h (*) g),f] by A9, Lm4
.= (CompMap C) . (((CompMap C) . (h,g)),f) by A11, BINOP_1:def 1 ; :: thesis: verum
end;
end;