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 ; ( 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)
; S1 = S2
A8:
the ResultSort of S1 = the ResultSort of S2
proof
thus
the
carrier' of
S1 = the
carrier' of
S2
by A4, A7;
FUNCT_2:def 7 for b1 being Element of the carrier' of S1 holds the ResultSort of S1 . b1 = the ResultSort of S2 . b1
let o be
OperSymbol of
S1;
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
;
verum
end;
the Arity of S1 = the Arity of S2
hence
S1 = S2
by A3, A6, A8; verum