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 ; ( 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
A13:
the carrier of S1 = P
and
A14:
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
A15:
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
A16:
the carrier of S2 = P
and
A17:
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
A18:
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] )
; S1 = S2
A19:
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)) }
by A14, FUNCT_2:def 1;
A20:
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 A17, FUNCT_2:def 1;
now for o being object st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } holds
the Arity of S1 . o = the Arity of S2 . olet o be
object ;
( 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)) }
;
the Arity of S1 . o = the Arity of S2 . othen consider f being
OperSymbol of
A,
p being
Element of
P * such that A21:
o = [f,p]
and A22:
product p meets dom (Den (f,A))
;
thus the
Arity of
S1 . o =
p
by A15, A21, A22
.=
the
Arity of
S2 . o
by A18, A21, A22
;
verum end;
then A23:
the Arity of S1 = the Arity of S2
by A19, A20;
A24:
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)) }
by A13, A14, FUNCT_2:def 1;
A25:
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 A16, A17, FUNCT_2:def 1;
consider R being Equivalence_Relation of the carrier of A such that
A26:
P = Class R
by EQREL_1:34;
now for o being object st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } holds
the ResultSort of S1 . o = the ResultSort of S2 . olet o be
object ;
( 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 A27:
o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) }
;
the ResultSort of S1 . o = the ResultSort of S2 . othen consider f being
OperSymbol of
A,
p being
Element of
P * such that A28:
o = [f,p]
and A29:
product p meets dom (Den (f,A))
;
consider x being
object such that A30:
x in product p
and A31:
x in dom (Den (f,A))
by A29, XBOOLE_0:3;
A32:
(Den (f,A)) . x in (Den (f,A)) .: (product p)
by A30, A31, FUNCT_1:def 6;
A33:
(Den (f,A)) .: (product p) c= the
ResultSort of
S1 . o
by A15, A28, A29;
A34:
(Den (f,A)) .: (product p) c= the
ResultSort of
S2 . o
by A18, A28, A29;
A35:
the
ResultSort of
S1 . o in P
by A13, A14, A27, FUNCT_2:5;
A36:
the
ResultSort of
S2 . o in P
by A16, A17, A27, FUNCT_2:5;
A37:
ex
y being
object st
(
y in the
carrier of
A & the
ResultSort of
S1 . o = Class (
R,
y) )
by A26, A35, EQREL_1:def 3;
A38:
ex
y being
object st
(
y in the
carrier of
A & the
ResultSort of
S2 . o = Class (
R,
y) )
by A26, A36, EQREL_1:def 3;
the
ResultSort of
S1 . o = Class (
R,
((Den (f,A)) . x))
by A32, A33, A37, EQREL_1:23;
hence
the
ResultSort of
S1 . o = the
ResultSort of
S2 . o
by A32, A34, A38, EQREL_1:23;
verum end;
hence
S1 = S2
by A13, A14, A16, A17, A23, A24, A25, FUNCT_1:2; verum