let C be non empty set ; :: thesis: for A being MSAlgebra over CatSign C
for a being Element of C holds Args ((idsym a),A) = {{}}
let A be MSAlgebra over CatSign C; :: thesis: for a being Element of C holds Args ((idsym a),A) = {{}}
let a be Element of C; :: thesis: Args ((idsym a),A) = {{}}
thus Args ((idsym a),A) = product ( the Sorts of A * (the_arity_of (idsym a))) by PRALG_2:3
.= product ( the Sorts of A * {}) by Def3
.= {{}} by CARD_3:10 ; :: thesis: verum