let X be RealUnitarySpace; :: thesis: NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) is RealNormSpace

set T = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #);

reconsider T = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) as non empty NORMSTR ;

A4: T is right_complementable

||.(0. X).|| = 0 by SQUARE_1:17, BHSP_1:1;

then A9: T is reflexive by Def1;

hence NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) is RealNormSpace by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10; :: thesis: verum

set T = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #);

reconsider T = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) as non empty NORMSTR ;

now :: thesis: for v, w being Element of T holds v + w = w + v

then A1:
T is Abelian
;let v, w be Element of T; :: thesis: v + w = w + v

reconsider v1 = v, w1 = w as Element of X ;

thus v + w = v1 + w1

.= w1 + v1

.= w + v ; :: thesis: verum

end;reconsider v1 = v, w1 = w as Element of X ;

thus v + w = v1 + w1

.= w1 + v1

.= w + v ; :: thesis: verum

now :: thesis: for u, v, w being Element of T holds (u + v) + w = u + (v + w)

then A2:
T is add-associative
;let u, v, w be Element of T; :: thesis: (u + v) + w = u + (v + w)

reconsider u1 = u, v1 = v, w1 = w as Element of X ;

thus (u + v) + w = (u1 + v1) + w1

.= u1 + (v1 + w1) by RLVECT_1:def 3

.= u + (v + w) ; :: thesis: verum

end;reconsider u1 = u, v1 = v, w1 = w as Element of X ;

thus (u + v) + w = (u1 + v1) + w1

.= u1 + (v1 + w1) by RLVECT_1:def 3

.= u + (v + w) ; :: thesis: verum

now :: thesis: for v being Element of T holds v + (0. T) = v

then A3:
T is right_zeroed
;let v be Element of T; :: thesis: v + (0. T) = v

reconsider v1 = v as Element of X ;

thus v + (0. T) = v1 + (0. X)

.= v ; :: thesis: verum

end;reconsider v1 = v as Element of X ;

thus v + (0. T) = v1 + (0. X)

.= v ; :: thesis: verum

A4: T is right_complementable

proof

let v be Element of T; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

reconsider v1 = v as Element of X ;

reconsider w1 = - v1 as Element of X ;

reconsider w = w1 as Element of T ;

take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. T

thus v + w = v1 + w1

.= 0. X by RLVECT_1:def 10

.= 0. T ; :: thesis: verum

end;reconsider v1 = v as Element of X ;

reconsider w1 = - v1 as Element of X ;

reconsider w = w1 as Element of T ;

take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. T

thus v + w = v1 + w1

.= 0. X by RLVECT_1:def 10

.= 0. T ; :: thesis: verum

now :: thesis: for a, b being Real

for v being Element of T holds (a + b) * v = (a * v) + (b * v)

then A5:
T is scalar-distributive
;for v being Element of T holds (a + b) * v = (a * v) + (b * v)

let a, b be Real; :: thesis: for v being Element of T holds (a + b) * v = (a * v) + (b * v)

let v be Element of T; :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider v1 = v as Element of X ;

thus (a + b) * v = (a + b) * v1

.= (a * v1) + (b * v1) by RLVECT_1:def 6

.= (a * v) + (b * v) ; :: thesis: verum

end;let v be Element of T; :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider v1 = v as Element of X ;

thus (a + b) * v = (a + b) * v1

.= (a * v1) + (b * v1) by RLVECT_1:def 6

.= (a * v) + (b * v) ; :: thesis: verum

now :: thesis: for a being Real

for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)

then A6:
T is vector-distributive
;for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)

let a be Real; :: thesis: for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)

let v, w be Element of T; :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider v1 = v, w1 = w as Element of X ;

thus a * (v + w) = a * (v1 + w1)

.= (a * v1) + (a * w1) by RLVECT_1:def 5

.= (a * v) + (a * w) ; :: thesis: verum

end;let v, w be Element of T; :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider v1 = v, w1 = w as Element of X ;

thus a * (v + w) = a * (v1 + w1)

.= (a * v1) + (a * w1) by RLVECT_1:def 5

.= (a * v) + (a * w) ; :: thesis: verum

now :: thesis: for a, b being Real

for v being Element of T holds (a * b) * v = a * (b * v)

then A7:
T is scalar-associative
;for v being Element of T holds (a * b) * v = a * (b * v)

let a, b be Real; :: thesis: for v being Element of T holds (a * b) * v = a * (b * v)

let v be Element of T; :: thesis: (a * b) * v = a * (b * v)

reconsider v1 = v as Element of X ;

thus (a * b) * v = (a * b) * v1

.= a * (b * v1) by RLVECT_1:def 7

.= a * (b * v) ; :: thesis: verum

end;let v be Element of T; :: thesis: (a * b) * v = a * (b * v)

reconsider v1 = v as Element of X ;

thus (a * b) * v = (a * b) * v1

.= a * (b * v1) by RLVECT_1:def 7

.= a * (b * v) ; :: thesis: verum

now :: thesis: for v being Element of T holds 1 * v = v

then A8:
T is scalar-unital
;let v be Element of T; :: thesis: 1 * v = v

reconsider v1 = v as Element of X ;

thus 1 * v = 1 * v1

.= v by RLVECT_1:def 8 ; :: thesis: verum

end;reconsider v1 = v as Element of X ;

thus 1 * v = 1 * v1

.= v by RLVECT_1:def 8 ; :: thesis: verum

||.(0. X).|| = 0 by SQUARE_1:17, BHSP_1:1;

then A9: T is reflexive by Def1;

now :: thesis: for v being Element of T st ||.v.|| = 0 holds

v = 0. T

then A10:
T is discerning
;v = 0. T

let v be Element of T; :: thesis: ( ||.v.|| = 0 implies v = 0. T )

assume AS: ||.v.|| = 0 ; :: thesis: v = 0. T

reconsider v1 = v as Element of X ;

||.v1.|| = 0 by AS, Def1;

then v1 = 0. X by BHSP_1:26;

hence v = 0. T ; :: thesis: verum

end;assume AS: ||.v.|| = 0 ; :: thesis: v = 0. T

reconsider v1 = v as Element of X ;

||.v1.|| = 0 by AS, Def1;

then v1 = 0. X by BHSP_1:26;

hence v = 0. T ; :: thesis: verum

now :: thesis: for a being Real

for v, w being Element of T holds

( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

then
T is RealNormSpace-like
;for v, w being Element of T holds

( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

let a be Real; :: thesis: for v, w being Element of T holds

( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

let v, w be Element of T; :: thesis: ( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

reconsider v1 = v, w1 = w as Element of X ;

thus ||.(a * v).|| = ||.(a * v1).|| by Def1

.= |.a.| * ||.v1.|| by BHSP_1:27

.= |.a.| * ||.v.|| by Def1 ; :: thesis: ||.(v + w).|| <= ||.v.|| + ||.w.||

C3: ||.(v + w).|| = ||.(v1 + w1).|| by Def1;

||.v.|| + ||.w.|| = ||.v1.|| + ((normRU X) . w) by Def1

.= ||.v1.|| + ||.w1.|| by Def1 ;

hence ||.(v + w).|| <= ||.v.|| + ||.w.|| by C3, BHSP_1:30; :: thesis: verum

end;( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

let v, w be Element of T; :: thesis: ( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

reconsider v1 = v, w1 = w as Element of X ;

thus ||.(a * v).|| = ||.(a * v1).|| by Def1

.= |.a.| * ||.v1.|| by BHSP_1:27

.= |.a.| * ||.v.|| by Def1 ; :: thesis: ||.(v + w).|| <= ||.v.|| + ||.w.||

C3: ||.(v + w).|| = ||.(v1 + w1).|| by Def1;

||.v.|| + ||.w.|| = ||.v1.|| + ((normRU X) . w) by Def1

.= ||.v1.|| + ||.w1.|| by Def1 ;

hence ||.(v + w).|| <= ||.v.|| + ||.w.|| by C3, BHSP_1:30; :: thesis: verum

hence NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) is RealNormSpace by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10; :: thesis: verum