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 )
set f1 = the carrier of S -indexing f;
set f2 = the carrier of S -indexing f;
set g1 = the carrier' of S -indexing g;
set g2 = the carrier' of S -indexing g;
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
A11:
the Arity of S1 = the Arity of S2
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 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;
:: thesis: the ResultSort of S1 . o = the ResultSort of S2 . o
consider o1 being
set such that A13:
(
o1 in dom (the carrier' of S -indexing g) &
o = (the carrier' of S -indexing g) . o1 )
by A4, FUNCT_1:def 5;
consider o2 being
set such that A14:
(
o2 in dom (the carrier' of S -indexing g) &
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, A13, A14, PUA2MSS1:def 13;
thus the
ResultSort of
S1 . o =
(the ResultSort of S1 * (the carrier' of S -indexing g)) . o1
by A13, 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, A13, A14, 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 A14, FUNCT_1:23
;
:: thesis: verum
end;
hence
S1 = S2
by A3, A4, A6, A7, A11; :: thesis: verum