let D be non empty set ; :: thesis: for d1, d2 being Element of D * holds (D -multiCat) . <*d1,d2*> = d1 ^ d2
let d1, d2 be Element of D * ; :: thesis: (D -multiCat) . <*d1,d2*> = d1 ^ d2
set F = D -multiCat ;
set f = D -concatenation ;
set d = <*d1,d2*>;
reconsider dd = <*d1*> ^ <*d2*> as non empty Element of (D *) * ;
A1: (D -multiCat) . dd = (MultPlace (D -concatenation)) . dd by Th14;
thus (D -multiCat) . <*d1,d2*> = (D -concatenation) . (((MultPlace (D -concatenation)) . <*d1*>),d2) by Lm15, A1
.= (D -concatenation) . (d1,d2) by Lm15
.= d1 ^ d2 by Lm10 ; :: thesis: verum