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 and
A2: g1 is one-to-one and
A3: f1,g1 form_morphism_between S1,S2 and
A4: the Sorts of C1 = the Sorts of C2 * f1 and
A5: the Charact of C1 = the Charact of C2 * g1 and
A6: f2 is one-to-one and
A7: g2 is one-to-one and
A8: f2,g2 form_morphism_between S2,S3 and
A9: the Sorts of C2 = the Sorts of C3 * f2 and
A10: 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, A2, A6, A7; :: 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 A3, A8, 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 A4, A5, A9, A10, RELAT_1:55; :: thesis: verum