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