let a be Real; :: thesis: ( |.|[0,a]|.| = abs a & |.|[a,0]|.| = abs a )
|.<*0,a*>.| = sqrt (Sum <*(0 ^2),(a ^2)*>) by Th16
.= sqrt (0 + (a ^2)) by RVSUM_1:107
.= abs a by COMPLEX1:158 ;
hence |.|[0,a]|.| = abs a ; :: thesis: |.|[a,0]|.| = abs a
|.<*a,0*>.| = sqrt (Sum <*(a ^2),(0 ^2)*>) by Th16
.= sqrt ((a ^2) + 0) by RVSUM_1:107
.= abs a by COMPLEX1:158 ;
hence |.|[a,0]|.| = abs a ; :: thesis: verum