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))) * ); :: thesis: ( ( 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 ) ) ) ) ) ) ) ; :: thesis: R = P
for x, y being set holds
( [x,y] in R iff [x,y] in P )

proof

let x, y be set ; :: thesis: ( [x,y] in R iff [x,y] in P )
thus ( [x,y] in R implies [x,y] in P ) :: thesis: ( [x,y] in P implies [x,y] in R )

proof

assume A4: [x,y] in R ; :: thesis: [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:106;
reconsider b = y as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by A4, ZFMISC_1:106;
[a,b] in R by A4;
then ( 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 ) ) ) ) ) ) by A2;
hence [x,y] in P by A3; :: thesis: verum

end;

assume A5: [x,y] in P ; :: thesis: [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:106;
reconsider b = y as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by A5, ZFMISC_1:106;
[a,b] in P by A5;
then ( 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 ) ) ) ) ) ) by A3;
hence [x,y] in R by A2; :: thesis: verum

end;

hence R = P by RELAT_1:def 2; :: thesis: verum