consider H being ManySortedFunction of F_{2}(),F_{3}() such that

A3: H is_homomorphism F_{2}(),F_{3}()
and

A4: F_{5}() = H ** F_{4}()
by A1, A2;

take H ; :: thesis: ( H is_homomorphism F_{2}(),F_{3}() & F_{5}() -hash = H ** (F_{4}() -hash) )

thus H is_homomorphism F_{2}(),F_{3}()
by A3; :: thesis: F_{5}() -hash = H ** (F_{4}() -hash)

F_{4}() -hash is_homomorphism FreeMSA ( the carrier of F_{1}() --> NAT),F_{2}()
by Def1;

then A5: H ** (F_{4}() -hash) is_homomorphism FreeMSA ( the carrier of F_{1}() --> NAT),F_{3}()
by A3, MSUALG_3:10;

reconsider SN = the carrier of F_{1}() --> NAT as V2() ManySortedSet of the carrier of F_{1}() ;

reconsider h1 = F_{5}() as ManySortedFunction of SN, the Sorts of F_{3}() ;

A6: h1 -hash is_homomorphism FreeMSA SN,F_{3}()
by Def1;

(h1 -hash) || (FreeGen SN) = F_{5}() ** (Reverse SN)
by Def1

.= H ** (F_{4}() ** (Reverse SN))
by A4, PBOOLE:140

.= H ** ((F_{4}() -hash) || (FreeGen ( the carrier of F_{1}() --> NAT)))
by Def1

.= (H ** (F_{4}() -hash)) || (FreeGen ( the carrier of F_{1}() --> NAT))
by EXTENS_1:4
;

hence F_{5}() -hash = H ** (F_{4}() -hash)
by A6, A5, EXTENS_1:14; :: thesis: verum

A3: H is_homomorphism F

A4: F

take H ; :: thesis: ( H is_homomorphism F

thus H is_homomorphism F

F

then A5: H ** (F

reconsider SN = the carrier of F

reconsider h1 = F

A6: h1 -hash is_homomorphism FreeMSA SN,F

(h1 -hash) || (FreeGen SN) = F

.= H ** (F

.= H ** ((F

.= (H ** (F

hence F