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 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 object 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 3;
consider o2 being object 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 3;
reconsider o1 = o1, o2 = o2 as OperSymbol of S by A9, A11;
thus the ResultSort of S1 . o = ( the ResultSort of S1 * ( the carrier' of S -indexing g)) . o1 by A9, A10, FUNCT_1:13
.= (( the carrier of S -indexing f) * the ResultSort of S) . o1 by A2
.= ( 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 A1, A10, A12, 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 A5
.= the ResultSort of S2 . o by A11, A12, 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 A4, A7; :: 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 object 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 3;
reconsider o2 = o2 as OperSymbol of S by A13;
thus the Arity of S1 . o = ( the carrier of S -indexing f) * (the_arity_of o2) by A2, A14
.= the Arity of S2 . o by A5, A14 ; :: thesis: verum

end;

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