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 non-empty 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:140
.= H ** ((F₄() -hash) || (FreeGen ( the carrier of F₁() --> NAT))) by Def1
.= (H ** (F₄() -hash)) || (FreeGen ( the carrier of F₁() --> NAT)) by EXTENS_1:4 ;
hence F₅() -hash = H ** (F₄() -hash) by A6, A5, EXTENS_1:14; :: thesis: verum