set O = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
let R, P be Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *); ( ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) & ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in P iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) implies R = P )
assume that
A2:
for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) )
and
A3:
for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in P iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) )
; R = P
for x, y being object holds
( [x,y] in R iff [x,y] in P )
proof
let x,
y be
object ;
( [x,y] in R iff [x,y] in P )
thus
(
[x,y] in R implies
[x,y] in P )
( [x,y] in P implies [x,y] in R )proof
assume A4:
[x,y] in R
;
[x,y] in P
then reconsider a =
x as
Element of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by ZFMISC_1:87;
reconsider b =
y as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A4, ZFMISC_1:87;
[a,b] in R
by A4;
then A5:
a in [: the carrier' of S,{ the carrier of S}:]
by A2;
for
o being
OperSymbol of
S st
[o, the carrier of S] = a holds
(
len b = len (the_arity_of o) & ( for
x being
set st
x in dom b holds
( (
b . x in [: the carrier' of S,{ the carrier of S}:] implies for
o1 being
OperSymbol of
S st
[o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & (
b . x in Union (coprod X) implies
b . x in coprod (
((the_arity_of o) . x),
X) ) ) ) )
by A2, A4;
hence
[x,y] in P
by A3, A5;
verum
end;
assume A6:
[x,y] in P
;
[x,y] in R
then reconsider a =
x as
Element of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by ZFMISC_1:87;
reconsider b =
y as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A6, ZFMISC_1:87;
[a,b] in P
by A6;
then A7:
a in [: the carrier' of S,{ the carrier of S}:]
by A3;
for
o being
OperSymbol of
S st
[o, the carrier of S] = a holds
(
len b = len (the_arity_of o) & ( for
x being
set st
x in dom b holds
( (
b . x in [: the carrier' of S,{ the carrier of S}:] implies for
o1 being
OperSymbol of
S st
[o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & (
b . x in Union (coprod X) implies
b . x in coprod (
((the_arity_of o) . x),
X) ) ) ) )
by A3, A6;
hence
[x,y] in R
by A2, A7;
verum
end;
hence
R = P
by RELAT_1:def 2; verum