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

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