let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of
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 ; :: 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 b' = b as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by Th2;
len b' = 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 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, 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