:: 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;