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