let C be non empty set ; :: thesis: for A being MSAlgebra of CatSign C
for a being Element of C holds Args (idsym a),A = {{} }
let A be MSAlgebra of 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:10
.= product (the Sorts of A * {} ) by Def5
.= {{} } by CARD_3:19 ; :: thesis: verum