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

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