let S1, S2, S3 be non empty ManySortedSign ; :: thesis: for f1, g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds
for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
let f1, g1 be Function; :: thesis: ( f1,g1 form_morphism_between S1,S2 implies for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds
for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) )
assume A1: f1,g1 form_morphism_between S1,S2 ; :: thesis: for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds
for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
let f2, g2 be Function; :: thesis: ( f2,g2 form_morphism_between S2,S3 implies for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) )
assume A2: f2,g2 form_morphism_between S2,S3 ; :: thesis: for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
A3: f2 * f1,g2 * g1 form_morphism_between S1,S3 by A1, A2, PUA2MSS1:29;
let A be MSAlgebra over S3; :: thesis: A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
A4: the Charact of ((A | (S2,f2,g2)) | (S1,f1,g1)) = the Charact of (A | (S2,f2,g2)) * g1 by A1, Def3
.= ( the Charact of A * g2) * g1 by A2, Def3
.= the Charact of A * (g2 * g1) by RELAT_1:36 ;
the Sorts of ((A | (S2,f2,g2)) | (S1,f1,g1)) = the Sorts of (A | (S2,f2,g2)) * f1 by A1, Def3
.= ( the Sorts of A * f2) * f1 by A2, Def3
.= the Sorts of A * (f2 * f1) by RELAT_1:36 ;
hence A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) by A3, A4, Def3; :: thesis: verum