let S1, S2, S3 be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of
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 ; :: 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 A3: f2 * f1,g2 * g1 form_morphism_between S1,S3 by A1, PUA2MSS1:30;
then A4: ( hom (f2 * f1),(g2 * g1),X,S1,S3 is_homomorphism FreeMSA (X * (f2 * f1)),(FreeMSA X) | S1,(f2 * f1),(g2 * g1) & hom f1,g1,(X * f2),S1,S2 is_homomorphism FreeMSA ((X * f2) * f1),(FreeMSA (X * f2)) | S1,f1,g1 & hom f2,g2,X,S2,S3 is_homomorphism FreeMSA (X * f2),(FreeMSA X) | S2,f2,g2 ) by A1, A2, Def5;
A5: 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;

reconsider Af = (FreeMSA X) | S1,(f2 * f1),(g2 * g1), Af1 = (FreeMSA (X * f2)) | S1,f1,g1 as non-empty MSAlgebra of S1 by A1, A2, Th23, PUA2MSS1:30;
(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
A6: ( hf1 = (hom f2,g2,X,S2,S3) * f1 & hf1 is_homomorphism Af1,Af ) by A1, A4, A5, Th35;
A7: X * (f2 * f1) = (X * f2) * f1 by RELAT_1:55;
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)) ;
A8: hf1 ** hh is_homomorphism FreeMSA (X * (f2 * f1)),Af by A4, A6, A7, MSUALG_3:10;

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)]
A9: ( (X * (f2 * f1)) . s = (X * f2) . (f1 . s) & (X * f2) . (f1 . s) = X . (f2 . (f1 . s)) ) by A7, FUNCT_2:21;
reconsider t = root-tree [x,s] as Term of S1,(X * (f2 * f1)) by MSATERM:4;
( the_sort_of t = s & (FreeSort (X * (f2 * f1))) . s = FreeSort (X * (f2 * f1)),s & FreeMSA (X * (f2 * f1)) = MSAlgebra(# (FreeSort (X * (f2 * f1))),(FreeOper (X * (f2 * f1))) #) ) by MSAFREE:def 13, MSAFREE:def 16, MSATERM:14;
then A10: root-tree [x,s] in the Sorts of (FreeMSA (X * (f2 * f1))) . s by MSATERM:def 5;
(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 A6, FUNCT_2:21
.= root-tree [x,(f2 . (f1 . s))] by A2, A9, Def5
.= root-tree [x,((f2 * f1) . s)] by FUNCT_2:21 ;
:: thesis: verum

end;

hence hom (f2 * f1),(g2 * g1),X,S1,S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2) by A3, A6, A8, Def5; :: thesis: verum