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 object holds

( [x,y] in R iff [x,y] in P )

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 object holds

( [x,y] in R iff [x,y] in P )

proof

hence
R = P
by RELAT_1:def 2; :: thesis: verum
let x, y be object ; :: 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 )

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; :: thesis: verum

end;thus ( [x,y] in R implies [x,y] in P ) :: thesis: ( [x,y] in P implies [x,y] in R )

proof

assume A6:
[x,y] in P
; :: thesis: [x,y] in R
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: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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum