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
A1: the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S1 and
A2: the carrier of S1 = rng ( the carrier of S -indexing f) and
A3: the carrier' of S1 = rng ( the carrier' of S -indexing g) and
A4: the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S2 and
A5: the carrier of S2 = rng ( the carrier of S -indexing f) and
A6: the carrier' of S2 = rng ( the carrier' of S -indexing g) ; :: thesis: S1 = S2
A7: the ResultSort of S1 = the ResultSort of S2

proof

thus the carrier' of S1 = the carrier' of S2 by A3, A6; :: according to FUNCT_2:def 7 :: 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
A8: o1 in dom ( the carrier' of S -indexing g) and
A9: o = ( the carrier' of S -indexing g) . o1 by A3, FUNCT_1:def 3;
consider o2 being set such that
A10: o2 in dom ( the carrier' of S -indexing g) and
A11: o = ( the carrier' of S -indexing g) . o2 by A3, FUNCT_1:def 3;
reconsider o1 = o1, o2 = o2 as OperSymbol of S by A8, A10;
thus the ResultSort of S1 . o = ( the ResultSort of S1 * ( the carrier' of S -indexing g)) . o1 by A8, A9, FUNCT_1:13
.= (( the carrier of S -indexing f) * the ResultSort of S) . o1 by A1, PUA2MSS1:def 12
.= ( the carrier of S -indexing f) . (the_result_sort_of o1) by FUNCT_2:15
.= ( the carrier of S -indexing f) . (the_result_sort_of o2) by X1, A9, A11, Th29
.= (( the carrier of S -indexing f) * the ResultSort of S) . o2 by FUNCT_2:15
.= ( the ResultSort of S2 * ( the carrier' of S -indexing g)) . o2 by A4, PUA2MSS1:def 12
.= the ResultSort of S2 . o by A10, A11, FUNCT_1:13 ; :: thesis: verum

end;

the Arity of S1 = the Arity of S2

proof

thus the carrier' of S1 = the carrier' of S2 by A3, A6; :: according to FUNCT_2:def 7 :: 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
A12: o2 in dom ( the carrier' of S -indexing g) and
A13: o = ( the carrier' of S -indexing g) . o2 by A3, FUNCT_1:def 3;
reconsider o2 = o2 as OperSymbol of S by A12;
thus the Arity of S1 . o = ( the carrier of S -indexing f) * (the_arity_of o2) by A1, A13, PUA2MSS1:def 12
.= the Arity of S2 . o by A4, A13, PUA2MSS1:def 12 ; :: thesis: verum

end;

hence S1 = S2 by A2, A3, A5, A6, A7; :: thesis: verum