set O = [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X));
defpred S₁[ 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₁[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