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