:: NORMSP_0 semantic presentation begin definition attrc1 is strict ; struct N-Str -> 1-sorted ; aggrN-Str(# carrier, normF #) -> N-Str ; sel normF c1 -> Function of the carrier of c1,REAL; end; op1 = 1 --> 0 by CARD_1:49; then reconsider f = op1 as Function of 1,REAL by FUNCOP_1:46; reconsider z = 0 as Element of 1 by CARD_1:49, TARSKI:def_1; registration cluster non empty strict for N-Str ; existence ex b1 being N-Str st ( not b1 is empty & b1 is strict ) proof take N-Str(# 1,f #) ; ::_thesis: ( not N-Str(# 1,f #) is empty & N-Str(# 1,f #) is strict ) thus ( not N-Str(# 1,f #) is empty & N-Str(# 1,f #) is strict ) ; ::_thesis: verum end; end; definition let X be non empty N-Str ; let x be Element of X; func||.x.|| -> Real equals :: NORMSP_0:def 1 the normF of X . x; coherence the normF of X . x is Real ; end; :: deftheorem defines ||. NORMSP_0:def_1_:_ for X being non empty N-Str for x being Element of X holds ||.x.|| = the normF of X . x; definition let X be non empty N-Str ; let f be the carrier of X -valued Function; func||.f.|| -> Function means :Def2: :: NORMSP_0:def 2 ( dom it = dom f & ( for e being set st e in dom it holds it . e = ||.(f /. e).|| ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for e being set st e in dom b1 holds b1 . e = ||.(f /. e).|| ) ) proof deffunc H1( set ) -> Real = ||.(f /. \$1).||; consider g being Function such that A1: dom g = dom f and A2: for x being set st x in dom f holds g . x = H1(x) from FUNCT_1:sch_3(); take g ; ::_thesis: ( dom g = dom f & ( for e being set st e in dom g holds g . e = ||.(f /. e).|| ) ) thus ( dom g = dom f & ( for e being set st e in dom g holds g . e = ||.(f /. e).|| ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for e being set st e in dom b1 holds b1 . e = ||.(f /. e).|| ) & dom b2 = dom f & ( for e being set st e in dom b2 holds b2 . e = ||.(f /. e).|| ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = dom f & ( for e being set st e in dom f1 holds f1 . e = ||.(f /. e).|| ) & dom f2 = dom f & ( for e being set st e in dom f2 holds f2 . e = ||.(f /. e).|| ) implies f1 = f2 ) assume that A3: dom f1 = dom f and A4: for e being set st e in dom f1 holds f1 . e = ||.(f /. e).|| and A5: dom f2 = dom f and A6: for e being set st e in dom f2 holds f2 . e = ||.(f /. e).|| ; ::_thesis: f1 = f2 thus dom f1 = dom f2 by A3, A5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in dom f1 or f1 . b1 = f2 . b1 ) let e be set ; ::_thesis: ( not e in dom f1 or f1 . e = f2 . e ) assume A7: e in dom f1 ; ::_thesis: f1 . e = f2 . e hence f1 . e = ||.(f /. e).|| by A4 .= f2 . e by A3, A5, A6, A7 ; ::_thesis: verum end; end; :: deftheorem Def2 defines ||. NORMSP_0:def_2_:_ for X being non empty N-Str for f being the carrier of b1 -valued Function for b3 being Function holds ( b3 = ||.f.|| iff ( dom b3 = dom f & ( for e being set st e in dom b3 holds b3 . e = ||.(f /. e).|| ) ) ); registration let X be non empty N-Str ; let f be the carrier of X -valued Function; cluster||.f.|| -> REAL -valued ; coherence ||.f.|| is REAL -valued proof let u be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not u in rng ||.f.|| or u in REAL ) assume u in rng ||.f.|| ; ::_thesis: u in REAL then consider e being set such that A1: e in dom ||.f.|| and A2: u = ||.f.|| . e by FUNCT_1:def_3; ||.f.|| . e = ||.(f /. e).|| by A1, Def2; hence u in REAL by A2; ::_thesis: verum end; end; definition let C be non empty set ; let X be non empty N-Str ; let f be PartFunc of C, the carrier of X; :: original: ||. redefine func||.f.|| -> PartFunc of C,REAL means :: NORMSP_0:def 3 ( dom it = dom f & ( for c being Element of C st c in dom it holds it . c = ||.(f /. c).|| ) ); coherence ||.f.|| is PartFunc of C,REAL proof dom ||.f.|| = dom f by Def2; then A1: dom ||.f.|| c= C by RELAT_1:def_18; rng ||.f.|| c= REAL proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng ||.f.|| or e in REAL ) assume e in rng ||.f.|| ; ::_thesis: e in REAL then consider u being set such that A2: u in dom ||.f.|| and A3: e = ||.f.|| . u by FUNCT_1:def_3; e = ||.(f /. u).|| by A2, A3, Def2; hence e in REAL ; ::_thesis: verum end; hence ||.f.|| is PartFunc of C,REAL by A1, RELSET_1:4; ::_thesis: verum end; compatibility for b1 being PartFunc of C,REAL holds ( b1 = ||.f.|| iff ( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 . c = ||.(f /. c).|| ) ) ) proof let F be PartFunc of C,REAL; ::_thesis: ( F = ||.f.|| iff ( dom F = dom f & ( for c being Element of C st c in dom F holds F . c = ||.(f /. c).|| ) ) ) thus ( F = ||.f.|| implies ( dom F = dom f & ( for c being Element of C st c in dom F holds F . c = ||.(f /. c).|| ) ) ) by Def2; ::_thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds F . c = ||.(f /. c).|| ) implies F = ||.f.|| ) assume that A4: dom F = dom f and A5: for c being Element of C st c in dom F holds F . c = ||.(f /. c).|| ; ::_thesis: F = ||.f.|| for e being set st e in dom F holds F . e = ||.(f /. e).|| proof let e be set ; ::_thesis: ( e in dom F implies F . e = ||.(f /. e).|| ) assume A6: e in dom F ; ::_thesis: F . e = ||.(f /. e).|| dom F c= C by RELAT_1:def_18; then reconsider c = e as Element of C by A6; thus F . e = ||.(f /. c).|| by A6, A5 .= ||.(f /. e).|| ; ::_thesis: verum end; hence F = ||.f.|| by A4, Def2; ::_thesis: verum end; end; :: deftheorem defines ||. NORMSP_0:def_3_:_ for C being non empty set for X being non empty N-Str for f being PartFunc of C, the carrier of X for b4 being PartFunc of C,REAL holds ( b4 = ||.f.|| iff ( dom b4 = dom f & ( for c being Element of C st c in dom b4 holds b4 . c = ||.(f /. c).|| ) ) ); definition let X be non empty N-Str ; let s be sequence of X; :: original: ||. redefine func||.s.|| -> Real_Sequence means :: NORMSP_0:def 4 for n being Element of NAT holds it . n = ||.(s . n).||; coherence ||.s.|| is Real_Sequence proof A1: dom ||.s.|| = dom s by Def2 .= NAT by PARTFUN1:def_2 ; rng ||.s.|| c= REAL by RELAT_1:def_19; hence ||.s.|| is Real_Sequence by A1, FUNCT_2:2; ::_thesis: verum end; compatibility for b1 being Real_Sequence holds ( b1 = ||.s.|| iff for n being Element of NAT holds b1 . n = ||.(s . n).|| ) proof let S be Real_Sequence; ::_thesis: ( S = ||.s.|| iff for n being Element of NAT holds S . n = ||.(s . n).|| ) A2: dom S = NAT by PARTFUN1:def_2; A3: dom s = NAT by PARTFUN1:def_2; thus ( S = ||.s.|| implies for n being Element of NAT holds S . n = ||.(s . n).|| ) ::_thesis: ( ( for n being Element of NAT holds S . n = ||.(s . n).|| ) implies S = ||.s.|| ) proof assume A4: S = ||.s.|| ; ::_thesis: for n being Element of NAT holds S . n = ||.(s . n).|| let n be Element of NAT ; ::_thesis: S . n = ||.(s . n).|| ||.s.|| . n = ||.(s /. n).|| by Def2, A2, A4; hence S . n = ||.(s . n).|| by A4; ::_thesis: verum end; assume A5: for n being Element of NAT holds S . n = ||.(s . n).|| ; ::_thesis: S = ||.s.|| for e being set st e in dom s holds S . e = ||.(s /. e).|| proof let e be set ; ::_thesis: ( e in dom s implies S . e = ||.(s /. e).|| ) assume A6: e in dom s ; ::_thesis: S . e = ||.(s /. e).|| then reconsider n = e as Element of NAT by PARTFUN1:def_2; thus S . e = ||.(s . n).|| by A5 .= ||.(s /. e).|| by A6, PARTFUN1:def_6 ; ::_thesis: verum end; hence S = ||.s.|| by A2, A3, Def2; ::_thesis: verum end; end; :: deftheorem defines ||. NORMSP_0:def_4_:_ for X being non empty N-Str for s being sequence of X for b3 being Real_Sequence holds ( b3 = ||.s.|| iff for n being Element of NAT holds b3 . n = ||.(s . n).|| ); definition attrc1 is strict ; struct N-ZeroStr -> N-Str , ZeroStr ; aggrN-ZeroStr(# carrier, ZeroF, normF #) -> N-ZeroStr ; end; registration cluster non empty strict for N-ZeroStr ; existence ex b1 being N-ZeroStr st ( not b1 is empty & b1 is strict ) proof take N-ZeroStr(# 1,z,f #) ; ::_thesis: ( not N-ZeroStr(# 1,z,f #) is empty & N-ZeroStr(# 1,z,f #) is strict ) thus ( not N-ZeroStr(# 1,z,f #) is empty & N-ZeroStr(# 1,z,f #) is strict ) ; ::_thesis: verum end; end; definition let X be non empty N-ZeroStr ; attrX is discerning means :: NORMSP_0:def 5 for x being Element of X st ||.x.|| = 0 holds x = 0. X; attrX is reflexive means :Def6: :: NORMSP_0:def 6 ||.(0. X).|| = 0 ; end; :: deftheorem defines discerning NORMSP_0:def_5_:_ for X being non empty N-ZeroStr holds ( X is discerning iff for x being Element of X st ||.x.|| = 0 holds x = 0. X ); :: deftheorem Def6 defines reflexive NORMSP_0:def_6_:_ for X being non empty N-ZeroStr holds ( X is reflexive iff ||.(0. X).|| = 0 ); registration cluster non empty strict discerning reflexive for N-ZeroStr ; existence ex b1 being non empty strict N-ZeroStr st ( b1 is reflexive & b1 is discerning ) proof reconsider S = N-ZeroStr(# 1,z,f #) as non empty strict N-ZeroStr ; take S ; ::_thesis: ( S is reflexive & S is discerning ) ||.(0. S).|| = 0 by CARD_1:49, FUNCOP_1:7; hence S is reflexive by Def6; ::_thesis: S is discerning let x be Element of S; :: according to NORMSP_0:def_5 ::_thesis: ( ||.x.|| = 0 implies x = 0. S ) thus ( ||.x.|| = 0 implies x = 0. S ) by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; end; registration let X be non empty reflexive N-ZeroStr ; cluster||.(0. X).|| -> zero ; coherence ||.(0. X).|| is empty by Def6; end;