let S1, S2, S3 be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S3
for f1 being Function of the carrier of S1,the carrier of S2
for g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2 being Function of the carrier of S2,the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2)
let X be V5() ManySortedSet of the carrier of S3; :: thesis: for f1 being Function of the carrier of S1,the carrier of S2
for g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2 being Function of the carrier of S2,the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2)
let f1 be Function of the carrier of S1,the carrier of S2; :: thesis: for g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2 being Function of the carrier of S2,the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2)
let g1 be Function; :: thesis: ( f1,g1 form_morphism_between S1,S2 implies for f2 being Function of the carrier of S2,the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2) )
assume A1: f1,g1 form_morphism_between S1,S2 ; :: thesis: for f2 being Function of the carrier of S2,the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2)
let f2 be Function of the carrier of S2,the carrier of S3; :: thesis: for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2)
let g2 be Function; :: thesis: ( f2,g2 form_morphism_between S2,S3 implies hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2) )
set f = f2 * f1;
set g = g2 * g1;
assume A2: f2,g2 form_morphism_between S2,S3 ; :: thesis: hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2)
then reconsider Af = (FreeMSA X) | S1,(f2 * f1),(g2 * g1), Af1 = (FreeMSA (X * f2)) | S1,f1,g1 as non-empty MSAlgebra of S1 by A1, Th23, PUA2MSS1:30;
A3: hom f2,g2,X,S2,S3 is_homomorphism FreeMSA (X * f2),(FreeMSA X) | S2,f2,g2 by A2, Def5;
A4: the Sorts of (FreeMSA (X * f2)) is_transformable_to the Sorts of ((FreeMSA X) | S2,f2,g2)

proof

let i be set ; :: according to PZFMISC1:def 3 :: thesis: ( not i in the carrier of S2 or not the Sorts of ((FreeMSA X) | S2,f2,g2) . i = {} or the Sorts of (FreeMSA (X * f2)) . i = {} )
assume i in the carrier of S2 ; :: thesis: ( not the Sorts of ((FreeMSA X) | S2,f2,g2) . i = {} or the Sorts of (FreeMSA (X * f2)) . i = {} )
then reconsider s = i as SortSymbol of S2 ;
the Sorts of ((FreeMSA X) | S2,f2,g2) . s = (the Sorts of (FreeMSA X) * f2) . s by A2, Def3;
hence ( not the Sorts of ((FreeMSA X) | S2,f2,g2) . i = {} or the Sorts of (FreeMSA (X * f2)) . i = {} ) ; :: thesis: verum

end;

(FreeMSA X) | S1,(f2 * f1),(g2 * g1) = ((FreeMSA X) | S2,f2,g2) | S1,f1,g1 by A1, A2, Th28;
then consider hf1 being ManySortedFunction of Af1,Af such that
A5: hf1 = (hom f2,g2,X,S2,S3) * f1 and
A6: hf1 is_homomorphism Af1,Af by A1, A3, A4, Th35;
reconsider hh = hom f1,g1,(X * f2),S1,S2 as ManySortedFunction of (FreeMSA (X * (f2 * f1))),Af1 by RELAT_1:55;
reconsider hf1h = hf1 ** hh as ManySortedFunction of (FreeMSA (X * (f2 * f1))),((FreeMSA X) | S1,(f2 * f1),(g2 * g1)) ;
A7: X * (f2 * f1) = (X * f2) * f1 by RELAT_1:55;

A8: now

let s be SortSymbol of S1; :: thesis: for x being Element of (X * (f2 * f1)) . s holds (hf1h . s) . (root-tree [x,s]) = root-tree [x,((f2 * f1) . s)]
let x be Element of (X * (f2 * f1)) . s; :: thesis: (hf1h . s) . (root-tree [x,s]) = root-tree [x,((f2 * f1) . s)]
reconsider t = root-tree [x,s] as Term of S1,(X * (f2 * f1)) by MSATERM:4;
A9: FreeMSA (X * (f2 * f1)) = MSAlgebra(# (FreeSort (X * (f2 * f1))),(FreeOper (X * (f2 * f1))) #) by MSAFREE:def 16;
( the_sort_of t = s & (FreeSort (X * (f2 * f1))) . s = FreeSort (X * (f2 * f1)),s ) by MSAFREE:def 13, MSATERM:14;
then A10: root-tree [x,s] in the Sorts of (FreeMSA (X * (f2 * f1))) . s by A9, MSATERM:def 5;
A11: (X * (f2 * f1)) . s = (X * f2) . (f1 . s) by A7, FUNCT_2:21;
(hf1h . s) . (root-tree [x,s]) = ((hf1 . s) * ((hom f1,g1,(X * f2),S1,S2) . s)) . (root-tree [x,s]) by MSUALG_3:2
.= (hf1 . s) . (((hom f1,g1,(X * f2),S1,S2) . s) . (root-tree [x,s])) by A7, A10, FUNCT_2:21
.= (hf1 . s) . (root-tree [x,(f1 . s)]) by A1, A7, Def5 ;
hence (hf1h . s) . (root-tree [x,s]) = ((hom f2,g2,X,S2,S3) . (f1 . s)) . (root-tree [x,(f1 . s)]) by A5, FUNCT_2:21
.= root-tree [x,(f2 . (f1 . s))] by A2, A11, Def5
.= root-tree [x,((f2 * f1) . s)] by FUNCT_2:21 ;
:: thesis: verum

end;

A12: f2 * f1,g2 * g1 form_morphism_between S1,S3 by A1, A2, PUA2MSS1:30;
hom f1,g1,(X * f2),S1,S2 is_homomorphism FreeMSA ((X * f2) * f1),(FreeMSA (X * f2)) | S1,f1,g1 by A1, Def5;
then hf1 ** hh is_homomorphism FreeMSA (X * (f2 * f1)),Af by A6, A7, MSUALG_3:10;
hence hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2) by A12, A5, A8, Def5; :: thesis: verum