let x be object ; 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 ; 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; 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; 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; ( 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 )
; AOFA_A00:def 8 ( not x in the Sorts of T . s or <*x*> in Args (o,T) )
assume A2:
x in the Sorts of T . s
; <*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; verum