set q = <*> the carrier of K;
deffunc H1( Element of NAT ) -> Element of the carrier of K = the addF of K $$ (p | $1);
let s be Element of K; :: thesis: ( s = Sum p iff s = the addF of K $$ p )
consider f being Function of NAT ,the carrier of K such that
A1: for i being Element of NAT holds f . i = H1(i) from FUNCT_2:sch 4();
hereby :: thesis: ( s = the addF of K $$ p implies s = Sum p )
defpred S1[ set , set ] means ex q being FinSequence of the carrier of K st
( q = p * (Sgm (dom (p | $1))) & $2 = Sum q );
assume A2: s = Sum p ; :: thesis: s = the addF of K $$ p
A3: dom p = Seg (len p) by FINSEQ_1:def 3;
A4: for x being Element of Fin NAT ex y being Element of K st S1[x,y]
proof
let B be Element of Fin NAT ; :: thesis: ex y being Element of K st S1[B,y]
per cases ( dom p = {} or dom p <> {} ) ;
suppose A5: dom p = {} ; :: thesis: ex y being Element of K st S1[B,y]
reconsider u = Sum (<*> the carrier of K) as Element of K ;
reconsider q = <*> the carrier of K as FinSequence of the carrier of K ;
take u ; :: thesis: S1[B,u]
take q ; :: thesis: ( q = p * (Sgm (dom (p | B))) & u = Sum q )
p = {} by A5;
hence q = p * (Sgm (dom (p | B))) ; :: thesis: u = Sum q
thus u = Sum q ; :: thesis: verum
end;
suppose dom p <> {} ; :: thesis: ex y being Element of K st S1[B,y]
then reconsider domp = dom p as non empty set ;
reconsider p9 = p as Function of domp,the carrier of K by FINSEQ_2:30;
A6: dom (p | B) c= dom p by RELAT_1:89;
then reconsider pB = p | B as FinSubsequence by A3, FINSEQ_1:def 12;
rng (Sgm (dom pB)) = dom pB by FINSEQ_1:71;
then reconsider p99 = Sgm (dom (p | B)) as FinSequence of domp by A6, FINSEQ_1:def 4;
reconsider q = p9 * p99 as FinSequence of the carrier of K ;
reconsider u = Sum q as Element of K ;
take u ; :: thesis: S1[B,u]
take q ; :: thesis: ( q = p * (Sgm (dom (p | B))) & u = Sum q )
thus ( q = p * (Sgm (dom (p | B))) & u = Sum q ) ; :: thesis: verum
end;
end;
end;
consider G being Function of (Fin NAT ),the carrier of K such that
A7: for B being Element of Fin NAT holds S1[B,G . B] from FUNCT_2:sch 3(A4);
A8: now
let B9 be Element of Fin NAT ; :: thesis: ( B9 c= dom p & B9 <> {} implies for x being Element of NAT st x in (dom p) \ B9 holds
G . (B9 \/ {x}) = the addF of K . (G . B9),(([#] p,(the_unity_wrt the addF of K)) . x) )
assume that
B9 c= dom p and
B9 <> {} ; :: thesis: for x being Element of NAT st x in (dom p) \ B9 holds
G . (B9 \/ {x}) = the addF of K . (G . B9),(([#] p,(the_unity_wrt the addF of K)) . x)
let x be Element of NAT ; :: thesis: ( x in (dom p) \ B9 implies G . (B9 \/ {x}) = the addF of K . (G . B9),(([#] p,(the_unity_wrt the addF of K)) . x) )
set f2 = Sgm (dom (p | (B9 \/ {x})));
set f3 = (Sgm (dom (p | (B9 \/ {x})))) -| x;
set f4 = (Sgm (dom (p | (B9 \/ {x})))) |-- x;
reconsider Y = (finSeg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}) as finite set ;
A9: Seg (len (Sgm (dom (p | (B9 \/ {x}))))) = dom (Sgm (dom (p | (B9 \/ {x})))) by FINSEQ_1:def 3;
set R = rng ((Sgm (dom (p | (B9 \/ {x})))) | Y);
set M = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y);
A10: rng (Sgm Y) = Y by FINSEQ_1:def 13;
dom (Sgm Y) = finSeg (card Y) by FINSEQ_3:45;
then dom ((Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y)) = Seg (card Y) by A9, A10, RELAT_1:46;
then reconsider M = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y) as FinSequence by FINSEQ_1:def 2;
( rng (Sgm (dom (p | (B9 \/ {x})))) c= NAT & rng M c= rng (Sgm (dom (p | (B9 \/ {x})))) ) by FINSEQ_1:def 4, RELAT_1:45;
then rng M c= NAT by XBOOLE_1:1;
then reconsider L = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y) as FinSequence of NAT by FINSEQ_1:def 4;
now
let y be set ; :: thesis: ( ( y in rng L implies y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) ) & ( y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) implies y in rng L ) )
hereby :: thesis: ( y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) implies y in rng L )
assume y in rng L ; :: thesis: y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y)
then consider x being set such that
A11: x in dom L and
A12: y = L . x by FUNCT_1:def 5;
x in dom (Sgm Y) by A11, FUNCT_1:21;
then A13: (Sgm Y) . x in Y by A10, FUNCT_1:def 5;
y = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . x) by A11, A12, FUNCT_1:22;
hence y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) by A9, A13, FUNCT_1:73; :: thesis: verum
end;
assume y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) ; :: thesis: y in rng L
then consider x being set such that
A14: x in dom ((Sgm (dom (p | (B9 \/ {x})))) | Y) and
A15: y = ((Sgm (dom (p | (B9 \/ {x})))) | Y) . x by FUNCT_1:def 5;
A16: x in (dom (Sgm (dom (p | (B9 \/ {x}))))) /\ Y by A14, RELAT_1:90;
then A17: x in Y by XBOOLE_0:def 4;
then consider z being set such that
A18: z in dom (Sgm Y) and
A19: x = (Sgm Y) . z by A10, FUNCT_1:def 5;
x in dom (Sgm (dom (p | (B9 \/ {x})))) by A16, XBOOLE_0:def 4;
then A20: z in dom ((Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y)) by A18, A19, FUNCT_1:21;
then L . z = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . z) by FUNCT_1:22
.= y by A15, A17, A19, FUNCT_1:72 ;
hence y in rng L by A20, FUNCT_1:def 5; :: thesis: verum
end;
then A21: rng L = rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) by TARSKI:2;
x in {x} by TARSKI:def 1;
then A22: x in B9 \/ {x} by XBOOLE_0:def 3;
dom (p | (B9 \/ {x})) = (dom p) /\ (B9 \/ {x}) by RELAT_1:90;
then dom (p | (B9 \/ {x})) c= dom p by XBOOLE_1:17;
then A23: dom (p | (B9 \/ {x})) c= Seg (len p) by FINSEQ_1:def 3;
then reconsider pB9x = p | (B9 \/ {x}) as FinSubsequence by FINSEQ_1:def 12;
rng (Sgm (dom (p | (B9 \/ {x})))) c= Seg (len p) by A23, FINSEQ_1:def 13;
then A24: rng (Sgm (dom (p | (B9 \/ {x})))) c= dom p by FINSEQ_1:def 3;
rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= rng (Sgm (dom (p | (B9 \/ {x})))) by RELAT_1:99;
then rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= dom p by A24, XBOOLE_1:1;
then A25: rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= Seg (len p) by FINSEQ_1:def 3;
( dom (p | (B9 \/ {x})) c= dom p & dom p = Seg (len p) ) by FINSEQ_1:def 3, RELAT_1:89;
then reconsider pp = p | (B9 \/ {x}) as FinSubsequence by FINSEQ_1:def 12;
A26: dom (p | B9) = (dom p) /\ B9 by RELAT_1:90;
A27: now
let l, m, k1, k2 be natural number ; :: thesis: ( 1 <= l & l < m & m <= len L & k1 = L . l & k2 = L . m implies k1 < k2 )
assume that
A28: 1 <= l and
A29: l < m and
A30: m <= len L and
A31: ( k1 = L . l & k2 = L . m ) ; :: thesis: k1 < k2
l <= len L by A29, A30, XXREAL_0:2;
then A32: l in dom L by A28, FINSEQ_3:27;
then A33: L . l = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . l) by FUNCT_1:22;
A34: (Sgm Y) . l in dom (Sgm (dom (p | (B9 \/ {x})))) by A32, FUNCT_1:21;
1 <= m by A28, A29, XXREAL_0:2;
then A35: m in dom L by A30, FINSEQ_3:27;
then A36: L . m = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . m) by FUNCT_1:22;
m in dom (Sgm Y) by A35, FUNCT_1:21;
then A37: m <= len (Sgm Y) by FINSEQ_3:27;
A38: (Sgm Y) . m in dom (Sgm (dom (p | (B9 \/ {x})))) by A35, FUNCT_1:21;
reconsider l = l, m = m as Element of NAT by ORDINAL1:def 13;
reconsider K1 = (Sgm Y) . l, K2 = (Sgm Y) . m as Element of NAT by A34, A38;
A39: 1 <= K1 by A34, FINSEQ_3:27;
A40: K2 <= len (Sgm (dom (p | (B9 \/ {x})))) by A38, FINSEQ_3:27;
K1 < K2 by A28, A29, A37, FINSEQ_1:def 13;
hence k1 < k2 by A23, A31, A33, A36, A39, A40, FINSEQ_1:def 13; :: thesis: verum
end;
assume A41: x in (dom p) \ B9 ; :: thesis: G . (B9 \/ {x}) = the addF of K . (G . B9),(([#] p,(the_unity_wrt the addF of K)) . x)
then A42: x in dom p by XBOOLE_0:def 5;
then reconsider D = dom p, E = rng p as non empty set by RELAT_1:65;
x in dom p by A41, XBOOLE_0:def 5;
then A43: {x} c= dom p by ZFMISC_1:37;
p . x = p /. x by A42, PARTFUN1:def 8;
then reconsider px = p . x as Element of K ;
A44: dom <*px*> = Seg 1 by FINSEQ_1:55;
rng <*x*> = {x} by FINSEQ_1:55;
then ( dom <*x*> = Seg 1 & rng <*x*> c= dom p ) by A42, FINSEQ_1:55, ZFMISC_1:37;
then A45: dom (p * <*x*>) = dom <*px*> by A44, RELAT_1:46;
A46: now
let e be set ; :: thesis: ( e in dom <*px*> implies (p * <*x*>) . e = <*px*> . e )
assume A47: e in dom <*px*> ; :: thesis: (p * <*x*>) . e = <*px*> . e
then A48: e = 1 by A44, FINSEQ_1:4, TARSKI:def 1;
thus (p * <*x*>) . e = p . (<*x*> . e) by A45, A47, FUNCT_1:22
.= p . x by A48, FINSEQ_1:57
.= <*px*> . e by A48, FINSEQ_1:57 ; :: thesis: verum
end;
reconsider x9 = x as Element of D by A41, XBOOLE_0:def 5;
reconsider p9 = p as Function of D,E by FUNCT_2:3;
A49: E c= the carrier of K by FINSEQ_1:def 4;
not x in B9 by A41, XBOOLE_0:def 5;
then A50: not x in dom (p | B9) by A26, XBOOLE_0:def 4;
A51: rng (Sgm (dom pp)) = dom pp by FINSEQ_1:71;
then A52: rng (Sgm (dom (p | (B9 \/ {x})))) c= dom p by RELAT_1:89;
dom pp = (dom p) /\ (B9 \/ {x}) by RELAT_1:90;
then A53: x in rng (Sgm (dom (p | (B9 \/ {x})))) by A51, A42, A22, XBOOLE_0:def 4;
then rng ((Sgm (dom (p | (B9 \/ {x})))) |-- x) c= rng (Sgm (dom (p | (B9 \/ {x})))) by FINSEQ_4:59;
then A54: rng ((Sgm (dom (p | (B9 \/ {x})))) |-- x) c= D by A52, XBOOLE_1:1;
rng ((Sgm (dom (p | (B9 \/ {x})))) -| x) c= rng (Sgm (dom (p | (B9 \/ {x})))) by A53, FINSEQ_4:51;
then rng ((Sgm (dom (p | (B9 \/ {x})))) -| x) c= D by A52, XBOOLE_1:1;
then reconsider f39 = (Sgm (dom (p | (B9 \/ {x})))) -| x, f49 = (Sgm (dom (p | (B9 \/ {x})))) |-- x as FinSequence of D by A54, FINSEQ_1:def 4;
consider q2 being FinSequence of the carrier of K such that
A55: q2 = p * (Sgm (dom (p | (B9 \/ {x})))) and
A56: G . (B9 \/ {.x.}) = Sum q2 by A7;
reconsider p3 = p9 * f39, p4 = p9 * f49 as FinSequence of E ;
rng p3 c= E by FINSEQ_1:def 4;
then A57: rng p3 c= the carrier of K by A49, XBOOLE_1:1;
rng p4 c= E by FINSEQ_1:def 4;
then rng p4 c= the carrier of K by A49, XBOOLE_1:1;
then reconsider p3 = p3, p4 = p4 as FinSequence of the carrier of K by A57, FINSEQ_1:def 4;
consider q1 being FinSequence of the carrier of K such that
A58: q1 = p * (Sgm (dom (p | B9))) and
A59: G . B9 = Sum q1 by A7;
A60: Sgm (dom (p | (B9 \/ {x}))) is one-to-one by A23, FINSEQ_3:99;
rng ((Sgm (dom (p | (B9 \/ {x})))) | ((Seg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}))) = (Sgm (dom (p | (B9 \/ {x})))) .: ((Seg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x})) by RELAT_1:148
.= (Sgm (dom (p | (B9 \/ {x})))) .: ((dom (Sgm (dom (p | (B9 \/ {x}))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x})) by FINSEQ_1:def 3
.= ((Sgm (dom (p | (B9 \/ {x})))) .: (dom (Sgm (dom (p | (B9 \/ {x})))))) \ {x} by SETWISEO:11
.= (rng (Sgm (dom pB9x))) \ {x} by RELAT_1:146
.= (dom (p | (B9 \/ {x}))) \ {x} by FINSEQ_1:71
.= ((dom p) /\ (B9 \/ {x})) \ {x} by RELAT_1:90
.= (((dom p) /\ B9) \/ ((dom p) /\ {x})) \ {x} by XBOOLE_1:23
.= (((dom p) /\ B9) \/ {x}) \ {x} by A43, XBOOLE_1:28
.= (dom (p | B9)) \ {x} by A26, XBOOLE_1:40
.= dom (p | B9) by A50, ZFMISC_1:65 ;
then Sgm (dom (p | B9)) = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm ((Seg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}))) by A25, A21, A27, FINSEQ_1:def 13
.= (Sgm (dom (p | (B9 \/ {x})))) * (Sgm ((dom (Sgm (dom (p | (B9 \/ {x}))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}))) by FINSEQ_1:def 3
.= (Sgm (dom (p | (B9 \/ {x})))) - {x} by FINSEQ_3:def 1
.= ((Sgm (dom (p | (B9 \/ {x})))) -| x) ^ ((Sgm (dom (p | (B9 \/ {x})))) |-- x) by A53, A60, FINSEQ_4:70 ;
then A61: q1 = p3 ^ p4 by A58, FINSEQOP:10;
q2 = p9 * ((f39 ^ <*x9*>) ^ f49) by A55, A53, FINSEQ_4:66
.= (p9 * (f39 ^ <*x9*>)) ^ (p9 * f49) by FINSEQOP:10
.= ((p9 * f39) ^ (p9 * <*x9*>)) ^ (p9 * f49) by FINSEQOP:10
.= (p3 ^ <*px*>) ^ p4 by A45, A46, FUNCT_1:9 ;
hence G . (B9 \/ {x}) = (Sum (p3 ^ <*px*>)) + (Sum p4) by A56, RLVECT_1:58
.= ((Sum p3) + (Sum <*px*>)) + (Sum p4) by RLVECT_1:58
.= ((Sum p3) + (Sum p4)) + (Sum <*px*>) by RLVECT_1:def 6
.= (Sum q1) + (Sum <*px*>) by A61, RLVECT_1:58
.= the addF of K . (Sum q1),px by RLVECT_1:61
.= the addF of K . (G . B9),(([#] p,(the_unity_wrt the addF of K)) . x) by A59, A42, SETWOP_2:22 ;
:: thesis: verum
end;
A62: now
let x be Element of NAT ; :: thesis: G . {b1} = ([#] p,(the_unity_wrt the addF of K)) . b1
consider q being FinSequence of the carrier of K such that
A63: q = p * (Sgm (dom (p | {x}))) and
A64: G . {.x.} = Sum q by A7;
X: {} c= Seg 0 ;
per cases ( not x in dom p or x in dom p ) ;
suppose A65: not x in dom p ; :: thesis: G . {b1} = ([#] p,(the_unity_wrt the addF of K)) . b1
then dom p misses {x} by ZFMISC_1:56;
then (dom p) /\ {x} = {} by XBOOLE_0:def 7;
then q = p * (Sgm {} ) by A63, RELAT_1:90
.= p * {} by FINSEQ_1:4, FINSEQ_1:72, X
.= <*> the carrier of K ;
hence G . {x} = 0. K by A64, RLVECT_1:60
.= the_unity_wrt the addF of K by Th9
.= ([#] p,(the_unity_wrt the addF of K)) . x by A65, SETWOP_2:22 ;
:: thesis: verum
end;
suppose A66: x in dom p ; :: thesis: G . {b1} = ([#] p,(the_unity_wrt the addF of K)) . b1
then p . x = p /. x by PARTFUN1:def 8;
then reconsider px = p . x as Element of K ;
A67: dom <*px*> = Seg 1 by FINSEQ_1:55;
rng <*x*> = {x} by FINSEQ_1:55;
then ( dom <*x*> = Seg 1 & rng <*x*> c= dom p ) by A66, FINSEQ_1:55, ZFMISC_1:37;
then A68: dom (p * <*x*>) = dom <*px*> by A67, RELAT_1:46;
A69: now
let e be set ; :: thesis: ( e in dom <*px*> implies (p * <*x*>) . e = <*px*> . e )
assume A70: e in dom <*px*> ; :: thesis: (p * <*x*>) . e = <*px*> . e
then A71: e = 1 by A67, FINSEQ_1:4, TARSKI:def 1;
thus (p * <*x*>) . e = p . (<*x*> . e) by A68, A70, FUNCT_1:22
.= p . x by A71, FINSEQ_1:57
.= <*px*> . e by A71, FINSEQ_1:57 ; :: thesis: verum
end;
A72: x <> 0 by A66, FINSEQ_3:27;
q = p * (Sgm ((dom p) /\ {x})) by A63, RELAT_1:90
.= p * (Sgm {x}) by A66, ZFMISC_1:52
.= p * <*x*> by A72, FINSEQ_3:50
.= <*px*> by A68, A69, FUNCT_1:9 ;
hence G . {x} = px by A64, RLVECT_1:61
.= ([#] p,(the_unity_wrt the addF of K)) . x by A66, SETWOP_2:22 ;
:: thesis: verum
end;
end;
end;
A73: now
let e be Element of K; :: thesis: ( e is_a_unity_wrt the addF of K implies e = G . {} )
assume A74: e is_a_unity_wrt the addF of K ; :: thesis: e = G . {}
0. K is_a_unity_wrt the addF of K by Th8;
then A75: e = 0. K by A74, BINOP_1:18;
X: {} c= Seg 0 ;
consider q being FinSequence of the carrier of K such that
A76: q = p * (Sgm (dom (p | ({}. NAT )))) and
A77: G . ({}. NAT ) = Sum q by A7;
q = p * (Sgm (dom {} )) by A76
.= p * {} by FINSEQ_1:4, FINSEQ_1:72, X
.= <*> the carrier of K ;
hence e = G . {} by A77, A75, RLVECT_1:60; :: thesis: verum
end;
consider q1 being FinSequence of the carrier of K such that
A78: q1 = p * (Sgm (dom (p | (dom p)))) and
A79: G . (findom p) = Sum q1 by A7;
A80: the addF of K is having_a_unity by Th10;
q1 = p * (Sgm (dom p)) by A78, RELAT_1:98
.= p * (Sgm (Seg (len p))) by FINSEQ_1:def 3
.= p * (idseq (len p)) by FINSEQ_3:54
.= p by FINSEQ_2:64 ;
hence s = the addF of K $$ (findom p),([#] p,(the_unity_wrt the addF of K)) by A2, A80, A79, A73, A62, A8, SETWISEO:def 3
.= the addF of K $$ p by Th10, SETWOP_2:def 2 ;
:: thesis: verum
end;
A81: p | (len p) = p | (Seg (len p)) by FINSEQ_1:def 15
.= p | (dom p) by FINSEQ_1:def 3
.= p by RELAT_1:98 ;
A82: now
let j be Element of NAT ; :: thesis: for a being Element of K st j < len p & a = p . (j + 1) holds
f . (j + 1) = (f . j) + a
let a be Element of K; :: thesis: ( j < len p & a = p . (j + 1) implies f . (j + 1) = (f . j) + a )
assume that
A83: j < len p and
A84: a = p . (j + 1) ; :: thesis: f . (j + 1) = (f . j) + a
A85: j + 1 <= len p by A83, NAT_1:13;
then A86: len (p | (j + 1)) = j + 1 by FINSEQ_1:80;
j <= j + 1 by NAT_1:11;
then A87: Seg j c= Seg (j + 1) by FINSEQ_1:7;
A88: p | j = p | (Seg j) by FINSEQ_1:def 15
.= (p | (Seg (j + 1))) | (Seg j) by A87, RELAT_1:103
.= (p | (j + 1)) | (Seg j) by FINSEQ_1:def 15 ;
A89: 1 <= j + 1 by NAT_1:11;
then A90: j + 1 in dom (p | (j + 1)) by A86, FINSEQ_3:27;
j + 1 in dom p by A85, A89, FINSEQ_3:27;
then a = p /. (j + 1) by A84, PARTFUN1:def 8
.= (p | (j + 1)) /. (j + 1) by A90, FINSEQ_4:85
.= (p | (j + 1)) . (j + 1) by A90, PARTFUN1:def 8 ;
then p | (j + 1) = (p | j) ^ <*a*> by A86, A88, FINSEQ_3:61;
hence f . (j + 1) = the addF of K $$ ((p | j) ^ <*a*>) by A1
.= the addF of K . (the addF of K $$ (p | j)),a by Th10, FINSOP_1:5
.= (f . j) + a by A1 ;
:: thesis: verum
end;
p | 0 = <*> the carrier of K ;
then A91: f . 0 = the addF of K $$ (<*> the carrier of K) by A1
.= the_unity_wrt the addF of K by Th10, FINSOP_1:11
.= 0. K by Th9 ;
assume s = the addF of K $$ p ; :: thesis: s = Sum p
then s = f . (len p) by A1, A81;
hence s = Sum p by A91, A82, RLVECT_1:def 13; :: thesis: verum