set g1 = the carrier' of S -indexing g;
set g2 = the carrier' of S -indexing g;
set f1 = the carrier of S -indexing f;
set f2 = the carrier of S -indexing f;
let S1, S2 be non empty non void strict ManySortedSign ; :: thesis: ( the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,S1 & the carrier of S1 = rng (the carrier of S -indexing f) & the carrier' of S1 = rng (the carrier' of S -indexing g) & the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,S2 & the carrier of S2 = rng (the carrier of S -indexing f) & the carrier' of S2 = rng (the carrier' of S -indexing g) implies S1 = S2 )
assume that
A2: the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,S1 and
A3: the carrier of S1 = rng (the carrier of S -indexing f) and
A4: the carrier' of S1 = rng (the carrier' of S -indexing g) and
A5: the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,S2 and
A6: the carrier of S2 = rng (the carrier of S -indexing f) and
A7: the carrier' of S2 = rng (the carrier' of S -indexing g) ; :: thesis: S1 = S2
A8: the ResultSort of S1 = the ResultSort of S2

proof

thus the carrier' of S1 = the carrier' of S2 by A4, A7; :: according to FUNCT_2:def 8 :: thesis: for b₁ being Element of the carrier' of S1 holds the ResultSort of S1 . b₁ = the ResultSort of S2 . b₁
let o be OperSymbol of S1; :: thesis: the ResultSort of S1 . o = the ResultSort of S2 . o
consider o1 being set such that
A9: o1 in dom (the carrier' of S -indexing g) and
A10: o = (the carrier' of S -indexing g) . o1 by A4, FUNCT_1:def 5;
consider o2 being set such that
A11: o2 in dom (the carrier' of S -indexing g) and
A12: o = (the carrier' of S -indexing g) . o2 by A4, FUNCT_1:def 5;
reconsider o1 = o1, o2 = o2 as OperSymbol of S by A2, A9, A11, PUA2MSS1:def 13;
thus the ResultSort of S1 . o = (the ResultSort of S1 * (the carrier' of S -indexing g)) . o1 by A9, A10, FUNCT_1:23
.= ((the carrier of S -indexing f) * the ResultSort of S) . o1 by A2, PUA2MSS1:def 13
.= (the carrier of S -indexing f) . (the_result_sort_of o1) by FUNCT_2:21
.= (the carrier of S -indexing f) . (the_result_sort_of o2) by A1, A10, A12, Th30
.= ((the carrier of S -indexing f) * the ResultSort of S) . o2 by FUNCT_2:21
.= (the ResultSort of S2 * (the carrier' of S -indexing g)) . o2 by A5, PUA2MSS1:def 13
.= the ResultSort of S2 . o by A11, A12, FUNCT_1:23 ; :: thesis: verum

end;

the Arity of S1 = the Arity of S2

proof

thus the carrier' of S1 = the carrier' of S2 by A4, A7; :: according to FUNCT_2:def 8 :: thesis: for b₁ being Element of the carrier' of S1 holds the Arity of S1 . b₁ = the Arity of S2 . b₁
let o be OperSymbol of S1; :: thesis: the Arity of S1 . o = the Arity of S2 . o
consider o2 being set such that
A13: o2 in dom (the carrier' of S -indexing g) and
A14: o = (the carrier' of S -indexing g) . o2 by A4, FUNCT_1:def 5;
reconsider o2 = o2 as OperSymbol of S by A2, A13, PUA2MSS1:def 13;
thus the Arity of S1 . o = (the carrier of S -indexing f) * (the_arity_of o2) by A2, A14, PUA2MSS1:def 13
.= the Arity of S2 . o by A5, A14, PUA2MSS1:def 13 ; :: thesis: verum

end;

hence S1 = S2 by A3, A4, A6, A7, A8; :: thesis: verum