let x be object ; :: thesis: for S being non empty non void ManySortedSign
for o being OperSymbol of S
for s, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s*>,r & x in the Sorts of T . s holds
<*x*> in Args (o,T)
let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for s, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s*>,r & x in the Sorts of T . s holds
<*x*> in Args (o,T)
let o be OperSymbol of S; :: thesis: for s, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s*>,r & x in the Sorts of T . s holds
<*x*> in Args (o,T)
let s, r be SortSymbol of S; :: thesis: for T being MSAlgebra over S st o is_of_type <*s*>,r & x in the Sorts of T . s holds
<*x*> in Args (o,T)
let T be MSAlgebra over S; :: thesis: ( o is_of_type <*s*>,r & x in the Sorts of T . s implies <*x*> in Args (o,T) )
assume A1: ( the Arity of S . o = <*s*> & the ResultSort of S . o = r ) ; :: according to AOFA_A00:def 8 :: thesis: ( not x in the Sorts of T . s or <*x*> in Args (o,T) )
assume A2: x in the Sorts of T . s ; :: thesis: <*x*> in Args (o,T)
A3: dom the Sorts of T = the carrier of S by PARTFUN1:def 2;
Args (o,T) = product ( the Sorts of T * (the_arity_of o)) by PRALG_2:3
.= product <*( the Sorts of T . s)*> by A1, A3, FINSEQ_2:34 ;
hence <*x*> in Args (o,T) by A2, FINSEQ_3:123; :: thesis: verum