A1: for A, B being Universal_Algebra st MSSign A = MSSign B holds
signature A = signature B
proof
let A, B be Universal_Algebra; :: thesis: ( MSSign A = MSSign B implies signature A = signature B )
reconsider ff1 = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by MSUALG_1:2;
reconsider gg1 = (*--> 0) * (signature B) as Function of (dom (signature B)),({0} *) by MSUALG_1:2;
A2: ( MSSign A = ManySortedSign(# {0},(dom (signature A)),ff1,((dom (signature A)) --> z) #) & MSSign B = ManySortedSign(# {0},(dom (signature B)),gg1,((dom (signature B)) --> z) #) ) by MSUALG_1:10;
assume A3: MSSign A = MSSign B ; :: thesis: signature A = signature B
now :: thesis: for i being Nat st i in dom (signature A) holds
(signature A) . i = (signature B) . i
let i be Nat; :: thesis: ( i in dom (signature A) implies (signature A) . i = (signature B) . i )
assume A4: i in dom (signature A) ; :: thesis: (signature A) . i = (signature B) . i
then reconsider k = (signature A) . i as Element of NAT by PARTFUN1:4;
A5: i in dom ((*--> 0) * (signature A)) by A4, FINSEQ_3:120;
then A6: (*--> 0) . ((signature B) . i) = ((*--> 0) * (signature A)) . i by A3, A2, FINSEQ_3:120
.= (*--> 0) . ((signature A) . i) by A5, FINSEQ_3:120 ;
reconsider m = (signature B) . i as Element of NAT by A3, A2, A4, PARTFUN1:4;
reconsider q = (*--> 0) . m as FinSequence ;
reconsider p = (*--> 0) . k as FinSequence ;
thus (signature A) . i = len p by Th6
.= len q by A6
.= (signature B) . i by Th6 ; :: thesis: verum
end;
hence signature A = signature B by A3, A2, FINSEQ_1:13; :: thesis: verum
end;
for A, B being Universal_Algebra st signature A = signature B holds
MSSign A = MSSign B by UNIALG_2:def 1, MSUHOM_1:10;
hence for A, B being Universal_Algebra holds
( signature A = signature B iff MSSign A = MSSign B ) by A1; :: thesis: verum