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