consider H being ManySortedFunction of F₂(),F₃() such that
A3: H is_homomorphism F₂(),F₃() and
A4: F₅() = H ** F₄() by A1, A2;
take H ; :: thesis: ( H is_homomorphism F₂(),F₃() & F₅() -hash = H ** (F₄() -hash ) )
thus H is_homomorphism F₂(),F₃() by A3; :: thesis: F₅() -hash = H ** (F₄() -hash )
F₄() -hash is_homomorphism FreeMSA (the carrier of F₁() --> NAT ),F₂() by Def1;
then A5: H ** (F₄() -hash ) is_homomorphism FreeMSA (the carrier of F₁() --> NAT ),F₃() by A3, MSUALG_3:10;
reconsider SN = the carrier of F₁() --> NAT as V8() ManySortedSet of the carrier of F₁() ;
reconsider h1 = F₅() as ManySortedFunction of SN,the Sorts of F₃() ;
A6: h1 -hash is_homomorphism FreeMSA SN,F₃() by Def1;
(h1 -hash ) || (FreeGen SN) = F₅() ** (Reverse SN) by Def1
.= H ** (F₄() ** (Reverse SN)) by A4, PBOOLE:154
.= H ** ((F₄() -hash ) || (FreeGen (the carrier of F₁() --> NAT ))) by Def1
.= (H ** (F₄() -hash )) || (FreeGen (the carrier of F₁() --> NAT )) by EXTENS_1:8 ;
hence F₅() -hash = H ** (F₄() -hash ) by A6, A5, EXTENS_1:18; :: thesis: verum