reconsider fi1 = F3() as ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2() ;
reconsider SN = the carrier of F1() --> NAT as V2() ManySortedSet of the carrier of F1() ;
let B be non-empty MSAlgebra over F1(); :: thesis: ( P1[B] implies B |= F5() '=' F6() )
assume P1[B] ; :: thesis: B |= F5() '=' F6()
then A3: P1[B] ;
let h be
ManySortedFunction of (TermAlg F1()),B; :: according to EQUATION:def 5 :: thesis: ( not h is_homomorphism TermAlg F1(),B or (h . F4()) . ((F5() '=' F6()) `1) = (h . F4()) . ((F5() '=' F6()) `2) )
assume A4: h is_homomorphism TermAlg F1(),B ; :: thesis: (h . F4()) . ((F5() '=' F6()) `1) = (h . F4()) . ((F5() '=' F6()) `2)
reconsider h1 = h as ManySortedFunction of (FreeMSA SN),B ;
set alfa = (h1 || (FreeGen SN)) ** ((Reverse SN) "");
A5: ((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash is_homomorphism FreeMSA SN,B by Def1;
reconsider alfa1 = (h1 || (FreeGen SN)) ** ((Reverse SN) "") as ManySortedFunction of the carrier of F1() --> NAT, the Sorts of B ;
A6: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds
ex h being ManySortedFunction of F2(),C st
( h is_homomorphism F2(),C & G = h ** fi1 ) by A2;
consider H being ManySortedFunction of F2(),B such that
H is_homomorphism F2(),B and
A7: alfa1 -hash = H ** (fi1 -hash) from A8: ((((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash) . F4()) . F5() = ((H . F4()) * ((F3() -hash) . F4())) . F5() by
.= (H . F4()) . (((F3() -hash) . F4()) . F6()) by
.= ((H . F4()) * ((F3() -hash) . F4())) . F6() by FUNCT_2:15
.= ((((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash) . F4()) . F6() by ;
rngs (Reverse SN) = SN by EXTENS_1:10;
then A9: ( Reverse SN is "1-1" & Reverse SN is "onto" ) by ;
(((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash) || (FreeGen SN) = ((h1 || (FreeGen SN)) ** ((Reverse SN) "")) ** (Reverse SN) by Def1
.= (h1 || (FreeGen SN)) ** (((Reverse SN) "") ** (Reverse SN)) by PBOOLE:140
.= (h1 || (FreeGen SN)) ** (id (FreeGen SN)) by
.= h1 || (FreeGen SN) by MSUALG_3:3 ;
then A10: ((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash = h1 by ;
thus (h . F4()) . ([F5(),F6()] `1) = (h . F4()) . F5()
.= (h . F4()) . ([F5(),F6()] `2) by ; :: thesis: verum