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

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