set O = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));

defpred S_{1}[ Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)), Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ] means ( $1 in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = $1 holds

( len $2 = len (the_arity_of o) & ( 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 o) . x ) & ( $2 . x in Union (coprod X) implies $2 . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) );

consider R being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) such that

A1: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in R iff S_{1}[a,b] )
from RELSET_1:sch 2();

take R ; :: thesis: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

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

( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( 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: ( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

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

thus ( [a,b] in R implies ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( 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) ) ) ) ) ) ) ) by A1; :: thesis: ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( 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 [a,b] in R )

assume ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( 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) ) ) ) ) ) ) ; :: thesis: [a,b] in R

hence [a,b] in R by A1; :: thesis: verum

defpred S

( len $2 = len (the_arity_of o) & ( 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 o) . x ) & ( $2 . x in Union (coprod X) implies $2 . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) );

consider R being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) such that

A1: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in R iff S

take R ; :: thesis: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

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

( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( 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: ( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

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

thus ( [a,b] in R implies ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( 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) ) ) ) ) ) ) ) by A1; :: thesis: ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( 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 [a,b] in R )

assume ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( 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) ) ) ) ) ) ) ; :: thesis: [a,b] in R

hence [a,b] in R by A1; :: thesis: verum