reconsider fi1 = F₃() as ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂() ;
reconsider SN = the carrier of F₁() --> NAT as non-empty ManySortedSet of the carrier of F₁() ;
let B be non-empty MSAlgebra over F₁(); :: thesis: ( P₁[B] implies B |= F₅() '=' F₆() )
assume P₁[B] ; :: thesis: B |= F₅() '=' F₆()
then A3: P₁[B] ;
let h be ManySortedFunction of (TermAlg F₁()),B; :: according to EQUATION:def 5 :: thesis: ( not h is_homomorphism TermAlg F₁(),B or (h . F₄()) . ((F₅() '=' F₆()) `1) = (h . F<sub>4</sub>()) . ((F<sub>5</sub>() '=' F<sub>6</sub>()) `2) )
assume A4: h is_homomorphism TermAlg F₁(),B ; :: thesis: (h . F₄()) . ((F₅() '=' F₆()) `1) = (h . F<sub>4</sub>()) . ((F<sub>5</sub>() '=' F<sub>6</sub>()) `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 F₁() --> NAT, the Sorts of B ;
A6: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of C st P₁[C] holds
ex h being ManySortedFunction of F₂(),C st
( h is_homomorphism F₂(),C & G = h ** fi1 ) by A2;
consider H being ManySortedFunction of F₂(),B such that
H is_homomorphism F₂(),B and
A7: alfa1 -hash = H ** (fi1 -hash) from BIRKHOFF:sch 3(A3, A6);
A8: ((((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash) . F₄()) . F₅() = ((H . F₄()) * ((F₃() -hash) . F₄())) . F₅() by A7, MSUALG_3:2
.= (H . F₄()) . (((F₃() -hash) . F₄()) . F₆()) by A1, FUNCT_2:15
.= ((H . F₄()) * ((F₃() -hash) . F₄())) . F₆() by FUNCT_2:15
.= ((((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash) . F₄()) . F₆() by A7, MSUALG_3:2 ;
rngs (Reverse SN) = SN by EXTENS_1:10;
then A9: ( Reverse SN is "1-1" & Reverse SN is "onto" ) by EXTENS_1:9, MSUALG_9:11;
(((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 A9, MSUALG_3:5
.= h1 || (FreeGen SN) by MSUALG_3:3 ;
then A10: ((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash = h1 by A4, A5, EXTENS_1:14;
thus (h . F₄()) . ([F₅(),F₆()] `1) = (h . F<sub>4</sub>()) . F<sub>5</sub>()
.= (h . F<sub>4</sub>()) . ([F<sub>5</sub>(),F<sub>6</sub>()] `2) by A10, A8 ; :: thesis: verum