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 of 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 of 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 of 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 of 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 of S3 holds A | S1,(f2 * f1),(g2 * g1) = (A | S2,f2,g2) | S1,f1,g1
let A be MSAlgebra of S3; :: thesis: 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:30;
A4: 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:55 ;
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:55 ;
hence A | S1,(f2 * f1),(g2 * g1) = (A | S2,f2,g2) | S1,f1,g1 by A3, A4, Def3; :: thesis: verum