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 FinSequence st [[o,the carrier of S],b] in REL X 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 X be ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for b being FinSequence st [[o,the carrier of S],b] in REL X 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 o be OperSymbol of S; :: thesis: for b being FinSequence st [[o,the carrier of S],b] in REL X 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 FinSequence; :: thesis: ( [[o,the carrier of S],b] in REL X implies ( 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 ) ) ) ) )
assume A1: [[o,the carrier of S],b] in REL X ; :: 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 ) ) ) )
then reconsider b9 = b as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by Th2;
len b9 = len (the_arity_of o) by A1, MSAFREE:5;
hence len b = len (the_arity_of o) ; :: thesis: 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 ) )
for x being set st x in dom b9 holds
( ( b9 . x in [:the carrier' of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b9 . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b9 . x in Union (coprod X) implies b9 . x in coprod ((the_arity_of o) . x),X ) ) by A1, MSAFREE:5;
hence 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: verum