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: MSAlg h1 is ManySortedSet of {0} by A1, Th17;
MSAlg h2 is ManySortedSet of {0} by A2, Th17;
then A4: dom (MSAlg h2) = {0} by PARTFUN1:def 2;
A5: dom ((MSAlg h2) ** (MSAlg h1)) = (dom (MSAlg h1)) /\ (dom (MSAlg h2)) by PBOOLE:def 19
.= {0} /\ {0} by A3, A4, PARTFUN1:def 2
.= {0} ;
A6: now :: thesis: for a being set
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 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
A7: a in dom ((MSAlg h2) ** (MSAlg h1)) and
A8: f = (MSAlg h1) . a and
A9: g = (MSAlg h2) . a ; :: thesis: ((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1
A10: g = (MSAlg h2) . 0 by A5, A7, A9, TARSKI:def 1
.= (0 .--> h2) . 0 by A2, Def3, Th10
.= h2 by FUNCOP_1:72 ;
f = (MSAlg h1) . 0 by A5, A7, A8, TARSKI:def 1
.= (0 .--> h1) . 0 by A1, Def3, Th10
.= h1 by FUNCOP_1:72 ;
hence ((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1 by A7, A8, A9, A10, PBOOLE:def 19; :: thesis: verum
end;
set h = h2 * h1;
A11: MSAlg (h2 * h1) is ManySortedSet of {0} by A1, A2, Th17, UNIALG_2:2;
A12: MSSign U2 = MSSign U3 by A2, Th10;
A13: now :: thesis: for a being set st a in dom (MSAlg (h2 * h1)) holds
(MSAlg (h2 * h1)) . a = h2 * h1
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 A14: a in {0} by A11, PARTFUN1:def 2;
(MSAlg (h2 * h1)) . 0 = (0 .--> (h2 * h1)) . 0 by A1, A12, Def3, Th10
.= h2 * h1 by FUNCOP_1:72 ;
hence (MSAlg (h2 * h1)) . a = h2 * h1 by A14, TARSKI:def 1; :: thesis: verum
end;
A15: dom (MSAlg (h2 * h1)) = {0} by A11, PARTFUN1:def 2;
A16: now :: thesis: for a being set
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 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
A17: a in dom (MSAlg (h2 * h1)) and
A18: ( f = (MSAlg h1) . a & g = (MSAlg h2) . a ) ; :: thesis: (MSAlg (h2 * h1)) . a = ((MSAlg h2) ** (MSAlg h1)) . a
thus (MSAlg (h2 * h1)) . a = h2 * h1 by A13, A17
.= ((MSAlg h2) ** (MSAlg h1)) . a by A5, A6, A15, A17, A18 ; :: thesis: verum
end;
A19: dom (MSAlg (h2 * h1)) = {0} by A11, PARTFUN1:def 2;
A20: for a being object st a in {0} holds
((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a
proof
let a be object ; :: thesis: ( a in {0} implies ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a )
A21: ( (MSAlg h1) . a is Function & (MSAlg h2) . a is Function ) ;
assume a in {0} ; :: thesis: ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a
hence ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a by A19, A16, A21; :: thesis: verum
end;
(MSAlg h2) ** (MSAlg h1) is ManySortedSet of {0} by A5, PARTFUN1:def 2, RELAT_1:def 18;
hence (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1) by A11, A20, PBOOLE:3; :: thesis: verum