let S1, S2, S3 be non empty ManySortedSign ; :: thesis: for f1, g1, f2, g2 being Function
for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2
for C3 being non-empty MSAlgebra of S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds
f2 * f1,g2 * g1 form_embedding_of C1,C3
let f1, g1, f2, g2 be Function; :: thesis: for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2
for C3 being non-empty MSAlgebra of S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds
f2 * f1,g2 * g1 form_embedding_of C1,C3
let C1 be non-empty MSAlgebra of S1; :: thesis: for C2 being non-empty MSAlgebra of S2
for C3 being non-empty MSAlgebra of S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds
f2 * f1,g2 * g1 form_embedding_of C1,C3
let C2 be non-empty MSAlgebra of S2; :: thesis: for C3 being non-empty MSAlgebra of S3 st f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 holds
f2 * f1,g2 * g1 form_embedding_of C1,C3
let C3 be non-empty MSAlgebra of S3; :: thesis: ( f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 implies f2 * f1,g2 * g1 form_embedding_of C1,C3 )
assume that
A1: ( f1 is one-to-one & g1 is one-to-one ) and
A2: f1,g1 form_morphism_between S1,S2 and
A3: the Sorts of C1 = the Sorts of C2 * f1 and
A4: the Charact of C1 = the Charact of C2 * g1 and
A5: ( f2 is one-to-one & g2 is one-to-one ) and
A6: f2,g2 form_morphism_between S2,S3 and
A7: the Sorts of C2 = the Sorts of C3 * f2 and
A8: the Charact of C2 = the Charact of C3 * g2 ; :: according to CIRCTRM1:def 12 :: thesis: f2 * f1,g2 * g1 form_embedding_of C1,C3
thus ( f2 * f1 is one-to-one & g2 * g1 is one-to-one ) by A1, A5; :: according to CIRCTRM1:def 12 :: thesis: ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & the Sorts of C1 = the Sorts of C3 * (f2 * f1) & the Charact of C1 = the Charact of C3 * (g2 * g1) )
thus f2 * f1,g2 * g1 form_morphism_between S1,S3 by A2, A6, PUA2MSS1:30; :: thesis: ( the Sorts of C1 = the Sorts of C3 * (f2 * f1) & the Charact of C1 = the Charact of C3 * (g2 * g1) )
thus ( the Sorts of C1 = the Sorts of C3 * (f2 * f1) & the Charact of C1 = the Charact of C3 * (g2 * g1) ) by A3, A4, A7, A8, RELAT_1:55; :: thesis: verum