let a be Real; :: thesis: a #Z 0 = 1
thus a #Z 0 = a |^ |.0.| by Def3
.= a |^ 0 by ABSVALUE:2
.= (a GeoSeq) . 0 by Def1
.= 1 by Th3 ; :: thesis: verum