reconsider SN = the carrier of F1() --> NAT as V8() ManySortedSet of ;
let B be non-empty MSAlgebra of F1(); :: thesis: ( P1[B] implies B |= F5() '=' F6() )
assume A3:
P1[B]
; :: thesis: B |= F5() '=' F6()
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) "" );
reconsider alfa1 = (h1 || (FreeGen SN)) ** ((Reverse SN) "" ) as ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of B ;
reconsider fi1 = F3() as ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of F2() ;
A5:
P1[B]
by A3;
A6:
for C being non-empty MSAlgebra of 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 BIRKHOFF:sch 3(A5, A6);
A8:
((h1 || (FreeGen SN)) ** ((Reverse SN) "" )) -hash is_homomorphism FreeMSA SN,B
by Def1;
rngs (Reverse SN) = SN
by EXTENS_1:14;
then A9:
( Reverse SN is "1-1" & Reverse SN is "onto" )
by EXTENS_1:13, MSUALG_9:12;
(((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:154
.=
(h1 || (FreeGen SN)) ** (id (FreeGen SN))
by A9, MSUALG_3:5
.=
h1 || (FreeGen SN)
by MSUALG_3:3
;
then A10:
((h1 || (FreeGen SN)) ** ((Reverse SN) "" )) -hash = h1
by A4, A8, EXTENS_1:18;
A11: ((((h1 || (FreeGen SN)) ** ((Reverse SN) "" )) -hash ) . F4()) . F5() =
((H . F4()) * ((F3() -hash ) . F4())) . F5()
by A7, MSUALG_3:2
.=
(H . F4()) . (((F3() -hash ) . F4()) . F6())
by A1, FUNCT_2:21
.=
((H . F4()) * ((F3() -hash ) . F4())) . F6()
by FUNCT_2:21
.=
((((h1 || (FreeGen SN)) ** ((Reverse SN) "" )) -hash ) . F4()) . F6()
by A7, MSUALG_3:2
;
thus (h . F4()) . ([F5(),F6()] `1 ) =
(h . F4()) . F5()
by MCART_1:7
.=
(h . F4()) . ([F5(),F6()] `2 )
by A10, A11, MCART_1:7
; :: thesis: verum