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 (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( 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) ) ) ) ) )
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 (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( 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) ) ) ) ) )
let o be OperSymbol of S; :: thesis: for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( 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) ) ) ) ) )
let b be Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ; :: thesis: ( [[o, the carrier of S],b] in REL X iff ( 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) ) ) ) ) )
defpred S₁[ OperSymbol of S, Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ] means ( len $2 = len (the_arity_of $1) & ( 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 = (the_arity_of $1) . x ) & ( $2 . x in Union (coprod X) implies b . x in coprod (((the_arity_of $1) . 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 (coprod X)) by XBOOLE_0:def 3;
thus ( [[o, the carrier of S],b] in REL X implies S₁[o,b] ) :: thesis: ( 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 [[o, the carrier of S],b] in REL X )

proof

assume [[o, the carrier of S],b] in REL X ; :: thesis: S₁[o,b]
then for o1 being OperSymbol of S st [o1, the carrier of S] = a holds
S₁[o1,b] by Def7;
hence S₁[o,b] ; :: thesis: verum

end;

assume A2: S₁[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
S₁[o1,b]

let o1 be OperSymbol of S; :: thesis: ( [o1, the carrier of S] = a implies S₁[o1,b] )
assume [o1, the carrier of S] = a ; :: thesis: S₁[o1,b]
then o1 = o by XTUPLE_0:1;
hence S₁[o1,b] by A2; :: thesis: verum

end;

hence [[o, the carrier of S],b] in REL X by A1, Def7; :: thesis: verum