let a be Real; :: thesis: ( |.|[0,a]|.| = |.a.| & |.|[a,0]|.| = |.a.| )
reconsider aa = a as Real ;
reconsider a2 = aa ^2 , z2 = 0 ^2 as Real ;
|.<*0,aa*>.| = sqrt (Sum <*z2,a2*>) by Th10
.= sqrt (0 + (a ^2)) by RVSUM_1:77
.= |.a.| by COMPLEX1:72 ;
hence |.|[0,a]|.| = |.a.| ; :: thesis: |.|[a,0]|.| = |.a.|
|.<*aa,0*>.| = sqrt (Sum <*a2,z2*>) by Th10
.= sqrt ((a ^2) + 0) by RVSUM_1:77
.= |.a.| by COMPLEX1:72 ;
hence |.|[a,0]|.| = |.a.| ; :: thesis: verum