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))

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;

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

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

(FreeMSA X) | (S1,(f2 * f1),(g2 * g1)) = ((FreeMSA X) | (S2,f2,g2)) | (S1,f1,g1)
by A1, A2, Th27;
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;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

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)]

A12:
f2 * f1,g2 * g1 form_morphism_between S1,S3
by A1, A2, PUA2MSS1:29;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;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

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