let U1, U2, U3 be Universal_Algebra; :: thesis: ( U1,U2 are_similar & U2,U3 are_similar implies for h1 being Function of U1,U2
for h2 being Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1) )
assume that
A1: U1,U2 are_similar and
A2: U2,U3 are_similar ; :: thesis: for h1 being Function of U1,U2
for h2 being Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1)
let h1 be Function of U1,U2; :: thesis: for h2 being Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1)
let h2 be Function of U2,U3; :: thesis: (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1)
A3: MSSign U2 = MSSign U3 by A2, Th10;
A4: MSAlg h1 is ManySortedSet of by A1, Th17;
MSAlg h2 is ManySortedSet of by A2, Th17;
then A5: dom (MSAlg h2) = {0 } by PARTFUN1:def 4;
A6: dom ((MSAlg h2) ** (MSAlg h1)) = (dom (MSAlg h1)) /\ (dom (MSAlg h2)) by PBOOLE:def 24
.= {0 } /\ {0 } by A4, A5, PARTFUN1:def 4
.= {0 } ;

A7: now

let a be set ; :: thesis: for f, g being Function st a in dom ((MSAlg h2) ** (MSAlg h1)) & f = (MSAlg h1) . a & g = (MSAlg h2) . a holds
((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1
let f, g be Function; :: thesis: ( a in dom ((MSAlg h2) ** (MSAlg h1)) & f = (MSAlg h1) . a & g = (MSAlg h2) . a implies ((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1 )
assume that
A8: a in dom ((MSAlg h2) ** (MSAlg h1)) and
A9: f = (MSAlg h1) . a and
A10: g = (MSAlg h2) . a ; :: thesis: ((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1
A11: f = (MSAlg h1) . 0 by A6, A8, A9, TARSKI:def 1
.= (0 .--> h1) . 0 by A1, Def3, Th10
.= h1 by FUNCOP_1:87 ;
g = (MSAlg h2) . 0 by A6, A8, A10, TARSKI:def 1
.= (0 .--> h2) . 0 by A2, Def3, Th10
.= h2 by FUNCOP_1:87 ;
hence ((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1 by A8, A9, A10, A11, PBOOLE:def 24; :: thesis: verum

end;

A12: (MSAlg h2) ** (MSAlg h1) is ManySortedSet of by A6, PARTFUN1:def 4, RELAT_1:def 18;
set h = h2 * h1;
A13: MSAlg (h2 * h1) is ManySortedSet of by A1, A2, Th17, UNIALG_2:4;
then A14: dom (MSAlg (h2 * h1)) = {0 } by PARTFUN1:def 4;

A15: now

let a be set ; :: thesis: ( a in dom (MSAlg (h2 * h1)) implies (MSAlg (h2 * h1)) . a = h2 * h1 )
assume a in dom (MSAlg (h2 * h1)) ; :: thesis: (MSAlg (h2 * h1)) . a = h2 * h1
then A16: a in {0 } by A13, PARTFUN1:def 4;
(MSAlg (h2 * h1)) . 0 = (0 .--> (h2 * h1)) . 0 by A1, A3, Def3, Th10
.= h2 * h1 by FUNCOP_1:87 ;
hence (MSAlg (h2 * h1)) . a = h2 * h1 by A16, TARSKI:def 1; :: thesis: verum

end;

A17: dom (MSAlg (h2 * h1)) = {0 } by A13, PARTFUN1:def 4;

A18: now

let a be set ; :: thesis: for f, g being Function st a in dom (MSAlg (h2 * h1)) & f = (MSAlg h1) . a & g = (MSAlg h2) . a holds
(MSAlg (h2 * h1)) . a = ((MSAlg h2) ** (MSAlg h1)) . a
let f, g be Function; :: thesis: ( a in dom (MSAlg (h2 * h1)) & f = (MSAlg h1) . a & g = (MSAlg h2) . a implies (MSAlg (h2 * h1)) . a = ((MSAlg h2) ** (MSAlg h1)) . a )
assume that
A19: a in dom (MSAlg (h2 * h1)) and
A20: f = (MSAlg h1) . a and
A21: g = (MSAlg h2) . a ; :: thesis: (MSAlg (h2 * h1)) . a = ((MSAlg h2) ** (MSAlg h1)) . a
thus (MSAlg (h2 * h1)) . a = h2 * h1 by A15, A19
.= ((MSAlg h2) ** (MSAlg h1)) . a by A6, A7, A14, A19, A20, A21 ; :: thesis: verum

end;

for a being set st a in {0 } holds
((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a

proof

let a be set ; :: thesis: ( a in {0 } implies ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a )
assume A22: a in {0 } ; :: thesis: ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a
A23: (MSAlg h1) . a is Function ;
(MSAlg h2) . a is Function ;
hence ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a by A17, A18, A22, A23; :: thesis: verum

end;

hence (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1) by A12, A13, PBOOLE:3; :: thesis: verum