let a be real number ; :: thesis: a #Z 0 = 1
thus a #Z 0 = a |^ (abs 0) by Def4
.= a |^ 0 by ABSVALUE:2
.= (a GeoSeq) . 0 by Def1
.= 1 by Th4 ; :: thesis: verum