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