set O = [: the carrier' of S,{ the carrier of S}:] \/ (Union ());
let R, P be Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) *); :: thesis: ( ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ())
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * 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 () & ( 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 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) ) ) ) & ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ())
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * 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 () & ( 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 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) ) ) ) implies R = P )

assume that
A2: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ())
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * 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 () & ( 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 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) ) ) and
A3: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ())
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * 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 () & ( 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 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) ) ) ; :: thesis: R = P
for x, y being object holds
( [x,y] in R iff [x,y] in P )
proof
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 )
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 ()) by ZFMISC_1:87;
reconsider b = y as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * by ;
[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 () & ( 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 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) by A2, A4;
hence [x,y] in P by A3, A5; :: thesis: verum
end;
assume A6: [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 ()) by ZFMISC_1:87;
reconsider b = y as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * by ;
[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 () & ( 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 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) by A3, A6;
hence [x,y] in R by A2, A7; :: thesis: verum
end;
hence R = P by RELAT_1:def 2; :: thesis: verum