let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type {} ,r holds
{} in Args (o,T)
let o be OperSymbol of S; :: thesis: for r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type {} ,r holds
{} in Args (o,T)
let r be SortSymbol of S; :: thesis: for T being MSAlgebra over S st o is_of_type {} ,r holds
{} in Args (o,T)
let T be MSAlgebra over S; :: thesis: ( o is_of_type {} ,r implies {} in Args (o,T) )
assume A1: ( the Arity of S . o = {} & the ResultSort of S . o = r ) ; :: according to AOFA_A00:def 8 :: thesis: {} in Args (o,T)
Args (o,T) = product ( the Sorts of T * (the_arity_of o)) by PRALG_2:3
.= {{}} by A1, CARD_3:10 ;
hence {} in Args (o,T) by TARSKI:def 1; :: thesis: verum