set O = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ;
let S1, S2 be strict ManySortedSign ; :: thesis: ( the carrier of S1 = P & the carrier' of S1 = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den o,A) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den o,A) holds
( the Arity of S1 . [o,p] = p & (Den o,A) .: (product p) c= the ResultSort of S1 . [o,p] ) ) & the carrier of S2 = P & the carrier' of S2 = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den o,A) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den o,A) holds
( the Arity of S2 . [o,p] = p & (Den o,A) .: (product p) c= the ResultSort of S2 . [o,p] ) ) implies S1 = S2 )
assume that
A12:
the carrier of S1 = P
and
A13:
the carrier' of S1 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) }
and
A14:
for f being OperSymbol of A
for p being Element of P * st product p meets dom (Den f,A) holds
( the Arity of S1 . [f,p] = p & (Den f,A) .: (product p) c= the ResultSort of S1 . [f,p] )
and
A15:
the carrier of S2 = P
and
A16:
the carrier' of S2 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) }
and
A17:
for f being OperSymbol of A
for p being Element of P * st product p meets dom (Den f,A) holds
( the Arity of S2 . [f,p] = p & (Den f,A) .: (product p) c= the ResultSort of S2 . [f,p] )
; :: thesis: S1 = S2
A18:
( dom the Arity of S1 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } & dom the Arity of S2 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } )
by A13, A16, FUNCT_2:def 1;
now let o be
set ;
:: thesis: ( o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } implies the Arity of S1 . o = the Arity of S2 . o )assume
o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) }
;
:: thesis: the Arity of S1 . o = the Arity of S2 . othen consider f being
OperSymbol of
A,
p being
Element of
P * such that A19:
(
o = [f,p] &
product p meets dom (Den f,A) )
;
thus the
Arity of
S1 . o =
p
by A14, A19
.=
the
Arity of
S2 . o
by A17, A19
;
:: thesis: verum end;
then A20:
the Arity of S1 = the Arity of S2
by A18, FUNCT_1:9;
A21:
( dom the ResultSort of S1 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } & dom the ResultSort of S2 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } )
by A12, A13, A15, A16, FUNCT_2:def 1;
consider R being Equivalence_Relation of the carrier of A such that
A22:
P = Class R
by EQREL_1:43;
now let o be
set ;
:: thesis: ( o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } implies the ResultSort of S1 . o = the ResultSort of S2 . o )assume A23:
o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) }
;
:: thesis: the ResultSort of S1 . o = the ResultSort of S2 . othen consider f being
OperSymbol of
A,
p being
Element of
P * such that A24:
(
o = [f,p] &
product p meets dom (Den f,A) )
;
consider x being
set such that A25:
(
x in product p &
x in dom (Den f,A) )
by A24, XBOOLE_0:3;
(
(Den f,A) . x in (Den f,A) .: (product p) &
(Den f,A) .: (product p) c= the
ResultSort of
S1 . o &
(Den f,A) .: (product p) c= the
ResultSort of
S2 . o & the
ResultSort of
S1 . o in P & the
ResultSort of
S2 . o in P )
by A12, A13, A14, A15, A16, A17, A23, A24, A25, FUNCT_1:def 12, FUNCT_2:7;
then
(
(Den f,A) . x in the
ResultSort of
S1 . o &
(Den f,A) . x in the
ResultSort of
S2 . o & ex
y being
set st
(
y in the
carrier of
A & the
ResultSort of
S1 . o = Class R,
y ) & ex
y being
set st
(
y in the
carrier of
A & the
ResultSort of
S2 . o = Class R,
y ) )
by A22, EQREL_1:def 5;
then
( the
ResultSort of
S1 . o = Class R,
((Den f,A) . x) & the
ResultSort of
S2 . o = Class R,
((Den f,A) . x) )
by EQREL_1:31;
hence
the
ResultSort of
S1 . o = the
ResultSort of
S2 . o
;
:: thesis: verum end;
hence
S1 = S2
by A12, A13, A15, A16, A20, A21, FUNCT_1:9; :: thesis: verum