let S1, S2, S3 be non empty non void ManySortedSign ; :: thesis: for X being V2() 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 V2() 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 over S1 by A1, Th22, PUA2MSS1:29;
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, Th27;
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, Th34;
reconsider hh = hom (f1,g1,(X * f2),S1,S2) as ManySortedFunction of (FreeMSA (X * (f2 * f1))),Af1 by RELAT_1:36;
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:36;
A8: now :: thesis: for s being SortSymbol of S1
for x being Element of (X * (f2 * f1)) . s holds (hf1h . s) . (root-tree [x,s]) = root-tree [x,((f2 * f1) . s)]
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 14;
( the_sort_of t = s & (FreeSort (X * (f2 * f1))) . s = FreeSort ((X * (f2 * f1)),s) ) by MSAFREE:def 11, 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:15;
(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:15
.= (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:15
.= root-tree [x,(f2 . (f1 . s))] by A2, A11, Def5
.= root-tree [x,((f2 * f1) . s)] by FUNCT_2:15 ;
:: thesis: verum
end;
A12: f2 * f1,g2 * g1 form_morphism_between S1,S3 by A1, A2, PUA2MSS1:29;
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