let S be OrderSortedSign; :: thesis: for X being ManySortedSet of
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 OSREL 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 ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,X ) ) ) ) ) )
let X be ManySortedSet of ; :: 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 OSREL 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 ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,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 OSREL 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 ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,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 OSREL 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 ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,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 ex i being Element of S st
( i <= (the_arity_of $1) /. x & b . x in coprod i,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 OSREL 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 ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,X ) ) ) ) implies [[o,the carrier of S],b] in OSREL X )

proof

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

end;

assume A2: S₁[o,b] ; :: thesis: [[o,the carrier of S],b] in OSREL 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 OSREL X by A1, Def4; :: thesis: verum