let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * holds
( [[o, the carrier of S],b] in REL X iff ( 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) ) ) ) ) )

let X be ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * holds
( [[o, the carrier of S],b] in REL X iff ( 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) ) ) ) ) )

let o be OperSymbol of S; :: thesis: for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * holds
( [[o, the carrier of S],b] in REL X iff ( 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) ) ) ) ) )

let b be Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * ; :: thesis: ( [[o, the carrier of S],b] in REL X iff ( 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) ) ) ) ) )

defpred S1[ OperSymbol of S, Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * ] means ( len \$2 = len () & ( for x being set st x in dom \$2 holds
( ( \$2 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = \$2 . x holds
the_result_sort_of o1 = () . x ) & ( \$2 . x in Union () implies b . x in coprod ((() . x),X) ) ) ) );
set a = [o, the carrier of S];
the carrier of S in { the carrier of S} by TARSKI:def 1;
then A1: [o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
then reconsider a = [o, the carrier of S] as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) by XBOOLE_0:def 3;
thus ( [[o, the carrier of S],b] in REL X implies S1[o,b] ) :: thesis: ( 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 [[o, the carrier of S],b] in REL X )
proof
assume [[o, the carrier of S],b] in REL X ; :: thesis: S1[o,b]
then for o1 being OperSymbol of S st [o1, the carrier of S] = a holds
S1[o1,b] by Def7;
hence S1[o,b] ; :: thesis: verum
end;
assume A2: S1[o,b] ; :: thesis: [[o, the carrier of S],b] in REL X
now :: thesis: for o1 being OperSymbol of S st [o1, the carrier of S] = a holds
S1[o1,b]
let o1 be OperSymbol of S; :: thesis: ( [o1, the carrier of S] = a implies S1[o1,b] )
assume [o1, the carrier of S] = a ; :: thesis: S1[o1,b]
then o1 = o by XTUPLE_0:1;
hence S1[o1,b] by A2; :: thesis: verum
end;
hence [[o, the carrier of S],b] in REL X by ; :: thesis: verum