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_{1}[ 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_{1}[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 )_{1}[o,b]
; :: thesis: [[o, the carrier of S],b] in REL X

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

( ( $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

( ( 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 A2:
S
assume
[[o, the carrier of S],b] in REL X
; :: thesis: S_{1}[o,b]

then for o1 being OperSymbol of S st [o1, the carrier of S] = a holds

S_{1}[o1,b]
by Def7;

hence S_{1}[o,b]
; :: thesis: verum

end;then for o1 being OperSymbol of S st [o1, the carrier of S] = a holds

S

hence S

now :: thesis: for o1 being OperSymbol of S st [o1, the carrier of S] = a holds

S_{1}[o1,b]

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

let o1 be OperSymbol of S; :: thesis: ( [o1, the carrier of S] = a implies S_{1}[o1,b] )

assume [o1, the carrier of S] = a ; :: thesis: S_{1}[o1,b]

then o1 = o by XTUPLE_0:1;

hence S_{1}[o1,b]
by A2; :: thesis: verum

end;assume [o1, the carrier of S] = a ; :: thesis: S

then o1 = o by XTUPLE_0:1;

hence S