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:106;
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 Def9;
hence S₁[o,b] ; :: thesis: verum

end;

assume A2: S₁[o,b] ; :: thesis: [[o,the carrier of S],b] in REL X

now

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 ZFMISC_1:33;
hence S₁[o1,b] by A2; :: thesis: verum

end;

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