thus ||.(0. N_Real).|| = 0 ; :: according to NORMSP_0:def 6 :: thesis:
thus for a being Element of N_Real st ||.a.|| = 0 holds
a = 0. N_Real ; :: according to NORMSP_0:def 5 :: thesis:
thus for a being Element of N_Real holds
( a * (1. N_Real) = a & (1. N_Real) * a = a ) ; :: according to VECTSP_1:def 6 :: thesis:
thus for a, b being Element of N_Real
for r being Real holds
( ||.(r * a).|| = |.r.| * ||.a.|| & ||.(a + b).|| <= ||.a.|| + ||.b.|| ) by COMPLEX1:56, COMPLEX1:65; :: according to NORMSP_1:def 1 :: thesis:
thus for a being Element of N_Real holds a + (0. N_Real) = a ; :: according to RLVECT_1:def 4 :: thesis:
thus for a, b, c being Element of N_Real holds a * (b + c) = (a * b) + (a * c) ; :: according to VECTSP_1:def 2 :: thesis:
thus for a, b being Element of N_Real
for r being Real holds r * (a * b) = (r * a) * b ; :: according to FUNCSDOM:def 9 :: thesis:
thus for r being Real
for a, b being Element of N_Real holds r * (a + b) = (r * a) + (r * b) ; :: according to RLVECT_1:def 5 :: thesis:
thus for r, s being Real
for a being Element of N_Real holds (r + s) * a = (r * a) + (s * a) ; :: according to RLVECT_1:def 6 :: thesis:
thus for r, s being Real
for a being Element of N_Real holds (r * s) * a = r * (s * a) ; :: according to RLVECT_1:def 7 :: thesis:
thus for a being Element of N_Real holds 1 * a = a ; :: according to RLVECT_1:def 8 :: thesis:
thus for a, b being Element of N_Real holds ||.(a * b).|| <= ||.a.|| * ||.b.|| by COMPLEX1:65; :: according to LOPBAN_2:def 9 :: thesis:
thus ||.(1. N_Real).|| = 1 by COMPLEX1:43; :: according to LOPBAN_2:def 10 :: thesis:
thus for r being Real
for a, b being Element of N_Real holds r * (a * b) = a * (r * b) ; :: according to LOPBAN_2:def 11 :: thesis:
thus for a being Element of N_Real st a <> 0. N_Real holds
ex b being Element of N_Real st b * a = 1. N_Real :: according to VECTSP_1:def 9 :: thesis:

proof

let a be Element of N_Real; :: thesis:
assume A1: a <> 0. N_Real ; :: thesis:
reconsider b = a " as Element of N_Real by XREAL_0:def 1;
take b ; :: thesis:
thus b * a = 1. N_Real by A1, XCMPLX_0:def 7; :: thesis:

end;

thus for a being Element of N_Real st a <> 0. N_Real holds
a is left_mult-cancelable by XCMPLX_1:5; :: according to ALGSTR_0:def 35 :: thesis:
thus N_Real is well-conjugated :: thesis:

proof

let a be Element of N_Real; :: according to CAYLDICK:def 4 :: thesis:

per cases ;
:: according to CAYLDICK:def 3

case not a is zero ; :: thesis:

thus (a *') * a = (||.a.|| ^2) * (1. N_Real) by Th8; :: thesis:

end;

case a is zero ; :: thesis:

hence a *' = 0. N_Real ; :: according to STRUCT_0:def 12 :: thesis:

end;

end;

end;

thus for a, b being Element of N_Real holds (a + b) *' = (a *') + (b *') ; :: according to CAYLDICK:def 5 :: thesis:
thus for a being Element of N_Real holds ||.(a *').|| = ||.a.|| ; :: according to CAYLDICK:def 6 :: thesis:
thus for r being Real
for a being Element of N_Real holds r * (a *') = (r * a) *' ; :: according to CAYLDICK:def 7 :: thesis: