set q = <*> the carrier of K;
deffunc H1( 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 sequence of the carrier of K such that
A1: for i being Element of NAT holds f . i = H1(i) from FUNCT_2:sch 4();
 A2: for i being Nat holds f . i = H1(i)
proof
let i be Nat; :: thesis: f . i = H1(i)
i in NAT by ORDINAL1:def 12;
hence f . i = H1(i) by A1; :: thesis: verum
end;
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 A3: s = Sum p ; :: thesis: s = the addF of K $$ p
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:26;
A6: dom (p | B) c= dom p by RELAT_1:60;
reconsider pB = p | B as FinSubsequence ;
rng (Sgm (dom pB)) = dom pB by FINSEQ_1:50;
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 :: thesis: for B9 being Element of Fin NAT st B9 c= dom p & B9 <> {} holds
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 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 14;
dom (Sgm Y) = finSeg (card Y) by FINSEQ_3:40;
then dom ((Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y)) = Seg (card Y) by A9, A10, RELAT_1:27;
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:26;
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 :: thesis: for y being object holds
( ( 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 ) )
let y be object ; :: 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 object such that
A11: x in dom L and
A12: y = L . x by FUNCT_1:def 3;
x in dom (Sgm Y) by A11, FUNCT_1:11;
then A13: (Sgm Y) . x in Y by A10, FUNCT_1:def 3;
y = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . x) by A11, A12, FUNCT_1:12;
hence y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) by A9, A13, FUNCT_1:50; :: thesis: verum
end;
assume y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) ; :: thesis: y in rng L
then consider x being object 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 3;
A16: x in (dom (Sgm (dom (p | (B9 \/ {x}))))) /\ Y by A14, RELAT_1:61;
then A17: x in Y by XBOOLE_0:def 4;
then consider z being object such that
A18: z in dom (Sgm Y) and
A19: x = (Sgm Y) . z by A10, FUNCT_1:def 3;
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:11;
then L . z = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . z) by FUNCT_1:12
.= y by A15, A17, A19, FUNCT_1:49 ;
hence y in rng L by A20, FUNCT_1:def 3; :: 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;
reconsider pB9x = p | (B9 \/ {x}) as FinSubsequence ;
reconsider pp = p | (B9 \/ {x}) as FinSubsequence ;
A26: dom (p | B9) = (dom p) /\ B9 by RELAT_1:61;
A27: now :: thesis: for l, m being Nat st 1 <= l & l < m & m <= len L holds
L . l < L . m
let l, m be Nat; :: thesis: ( 1 <= l & l < m & m <= len L implies L . l < L . m )
assume that
A28: 1 <= l and
A29: l < m and
A30: m <= len L ; :: thesis: L . l < L . m
set k1 = L . l;
set k2 = L . m;
l <= len L by A29, A30, XXREAL_0:2;
then A32: l in dom L by A28, FINSEQ_3:25;
then A33: L . l = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . l) by FUNCT_1:12;
A34: (Sgm Y) . l in dom (Sgm (dom (p | (B9 \/ {x})))) by A32, FUNCT_1:11;
1 <= m by A28, A29, XXREAL_0:2;
then A35: m in dom L by A30, FINSEQ_3:25;
then A36: L . m = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . m) by FUNCT_1:12;
m in dom (Sgm Y) by A35, FUNCT_1:11;
then A37: m <= len (Sgm Y) by FINSEQ_3:25;
A38: (Sgm Y) . m in dom (Sgm (dom (p | (B9 \/ {x})))) by A35, FUNCT_1:11;
reconsider l = l, m = m as Element of NAT by ORDINAL1:def 12;
reconsider K1 = (Sgm Y) . l, K2 = (Sgm Y) . m as Element of NAT by A34, A38;
A39: 1 <= K1 by A34, FINSEQ_3:25;
A40: K2 <= len (Sgm (dom (p | (B9 \/ {x})))) by A38, FINSEQ_3:25;
K1 < K2 by A28, A29, A37, FINSEQ_1:def 14;
hence L . l < L . m by A33, A36, A39, A40, FINSEQ_1:def 14; :: 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:42;
x in dom p by A41, XBOOLE_0:def 5;
then A43: {x} c= dom p by ZFMISC_1:31;
p . x = p /. x by A42, PARTFUN1:def 6;
then reconsider px = p . x as Element of K ;
A44: dom <*px*> = Seg 1 by FINSEQ_1:38;
rng <*x*> = {x} by FINSEQ_1:38;
then ( dom <*x*> = Seg 1 & rng <*x*> c= dom p ) by A42, FINSEQ_1:38, ZFMISC_1:31;
then A45: dom (p * <*x*>) = dom <*px*> by A44, RELAT_1:27;
A46: now :: thesis: for e being object st e in dom <*px*> holds
(p * <*x*>) . e = <*px*> . e
let e be object ; :: 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:2, TARSKI:def 1;
thus (p * <*x*>) . e = p . (<*x*> . e) by A45, A47, FUNCT_1:12
.= p . x by A48
.= <*px*> . e by A48 ; :: 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:1;
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:50;
then A52: rng (Sgm (dom (p | (B9 \/ {x})))) c= dom p by RELAT_1:60;
dom pp = (dom p) /\ (B9 \/ {x}) by RELAT_1:61;
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:44;
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:39;
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 FINSEQ_3:92;
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:115
.= (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:6
.= (rng (Sgm (dom pB9x))) \ {x} by RELAT_1:113
.= (dom (p | (B9 \/ {x}))) \ {x} by FINSEQ_1:50
.= ((dom p) /\ (B9 \/ {x})) \ {x} by RELAT_1:61
.= (((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:57 ;
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 A21, A27, FINSEQ_1:def 14
.= (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:55 ;
then A61: q1 = p3 ^ p4 by A58, FINSEQOP:9;
q2 = p9 * ((f39 ^ <*x9*>) ^ f49) by A55, A53, FINSEQ_4:51
.= (p9 * (f39 ^ <*x9*>)) ^ (p9 * f49) by FINSEQOP:9
.= ((p9 * f39) ^ (p9 * <*x9*>)) ^ (p9 * f49) by FINSEQOP:9
.= (p3 ^ <*px*>) ^ p4 by A45, A46, FUNCT_1:2 ;
hence G . (B9 \/ {x}) = (Sum (p3 ^ <*px*>)) + (Sum p4) by A56, RLVECT_1:41
.= ((Sum p3) + (Sum <*px*>)) + (Sum p4) by RLVECT_1:41
.= ((Sum p3) + (Sum p4)) + (Sum <*px*>) by RLVECT_1:def 3
.= (Sum q1) + (Sum <*px*>) by A61, RLVECT_1:41
.= the addF of K . ((Sum q1),px) by RLVECT_1:44
.= the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x)) by A59, A42, SETWOP_2:20 ;
:: thesis: verum
end;
A62: now :: thesis: for x being Element of NAT holds G . {x} = ([#] (p,(the_unity_wrt the addF of K))) . x
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;
per cases ( not x in dom p or x in dom p ) ;
suppose A66: 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:50;
then (dom p) /\ {x} = {} by XBOOLE_0:def 7;
then q = p * (Sgm {}) by A63, RELAT_1:61
.= p * {} by FINSEQ_1:51
.= <*> the carrier of K ;
hence G . {x} = 0. K by A64, RLVECT_1:43
.= the_unity_wrt the addF of K by Th7
.= ([#] (p,(the_unity_wrt the addF of K))) . x by A66, SETWOP_2:20 ;
:: thesis: verum
end;
suppose A67: x in dom p ; :: thesis: G . {b1} = ([#] (p,(the_unity_wrt the addF of K))) . b1
then p . x = p /. x by PARTFUN1:def 6;
then reconsider px = p . x as Element of K ;
A68: dom <*px*> = Seg 1 by FINSEQ_1:38;
rng <*x*> = {x} by FINSEQ_1:38;
then ( dom <*x*> = Seg 1 & rng <*x*> c= dom p ) by A67, FINSEQ_1:38, ZFMISC_1:31;
then A69: dom (p * <*x*>) = dom <*px*> by A68, RELAT_1:27;
A70: now :: thesis: for e being object st e in dom <*px*> holds
(p * <*x*>) . e = <*px*> . e
let e be object ; :: thesis: ( e in dom <*px*> implies (p * <*x*>) . e = <*px*> . e )
assume A71: e in dom <*px*> ; :: thesis: (p * <*x*>) . e = <*px*> . e
then A72: e = 1 by A68, FINSEQ_1:2, TARSKI:def 1;
thus (p * <*x*>) . e = p . (<*x*> . e) by A69, A71, FUNCT_1:12
.= p . x by A72
.= <*px*> . e by A72 ; :: thesis: verum
end;
A73: x <> 0 by A67, FINSEQ_3:25;
q = p * (Sgm ((dom p) /\ {x})) by A63, RELAT_1:61
.= p * (Sgm {x}) by A67, ZFMISC_1:46
.= p * <*x*> by A73, FINSEQ_3:44
.= <*px*> by A69, A70, FUNCT_1:2 ;
hence G . {x} = px by A64, RLVECT_1:44
.= ([#] (p,(the_unity_wrt the addF of K))) . x by A67, SETWOP_2:20 ;
:: thesis: verum
end;
end;
end;
A74: now :: thesis: for e being Element of K st e is_a_unity_wrt the addF of K holds
e = G . {}
let e be Element of K; :: thesis: ( e is_a_unity_wrt the addF of K implies e = G . {} )
assume A75: e is_a_unity_wrt the addF of K ; :: thesis: e = G . {}
0. K is_a_unity_wrt the addF of K by Th6;
then A76: e = 0. K by A75, BINOP_1:10;
consider q being FinSequence of the carrier of K such that
A78: q = p * (Sgm (dom (p | ({}. NAT)))) and
A79: G . ({}. NAT) = Sum q by A7;
q = p * (Sgm (dom {})) by A78
.= p * {} by FINSEQ_1:51
.= <*> the carrier of K ;
hence e = G . {} by A79, A76, RLVECT_1:43; :: thesis: verum
end;
consider q1 being FinSequence of the carrier of K such that
A80: q1 = p * (Sgm (dom (p | (dom p)))) and
A81: G . (findom p) = Sum q1 by A7;
A82: the addF of K is having_a_unity by Th8;
q1 = p * (Sgm (dom p)) by A80
.= p * (Sgm (Seg (len p))) by FINSEQ_1:def 3
.= p * (idseq (len p)) by FINSEQ_3:48
.= p by FINSEQ_2:54 ;
hence s = the addF of K $$ ((findom p),([#] (p,(the_unity_wrt the addF of K)))) by A3, A82, A81, A74, A62, A8, SETWISEO:def 3
.= the addF of K $$ p by Th8, SETWOP_2:def 2 ;
:: thesis: verum
end;
A83: p | (len p) = p | (Seg (len p)) by FINSEQ_1:def 16
.= p | (dom p) by FINSEQ_1:def 3
.= p ;
A84: now :: thesis: for j being Nat
for a being Element of K st j < len p & a = p . (j + 1) holds
f . (j + 1) = (f . j) + a
let j be 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
A85: j < len p and
A86: a = p . (j + 1) ; :: thesis: f . (j + 1) = (f . j) + a
A87: j + 1 <= len p by A85, NAT_1:13;
then A88: len (p | (j + 1)) = j + 1 by FINSEQ_1:59;
j <= j + 1 by NAT_1:11;
then A89: Seg j c= Seg (j + 1) by FINSEQ_1:5;
A90: p | j = p | (Seg j) by FINSEQ_1:def 16
.= (p | (Seg (j + 1))) | (Seg j) by A89, RELAT_1:74
.= (p | (j + 1)) | (Seg j) by FINSEQ_1:def 16 ;
A91: 1 <= j + 1 by NAT_1:11;
then A92: j + 1 in dom (p | (j + 1)) by A88, FINSEQ_3:25;
j + 1 in dom p by A87, A91, FINSEQ_3:25;
then a = p /. (j + 1) by A86, PARTFUN1:def 6
.= (p | (j + 1)) /. (j + 1) by A92, FINSEQ_4:70
.= (p | (j + 1)) . (j + 1) by A92, PARTFUN1:def 6 ;
then p | (j + 1) = (p | j) ^ <*a*> by A88, A90, FINSEQ_3:55;
hence f . (j + 1) = the addF of K $$ ((p | j) ^ <*a*>) by A2
.= the addF of K . (( the addF of K $$ (p | j)),a) by Th8, FINSOP_1:4
.= (f . j) + a by A2 ;
:: thesis: verum
end;
p | 0 = <*> the carrier of K ;
then A93: f . 0 = the addF of K $$ (<*> the carrier of K) by A2
.= the_unity_wrt the addF of K by Th8, FINSOP_1:10
.= 0. K by Th7 ;
assume s = the addF of K $$ p ; :: thesis: s = Sum p
then s = f . (len p) by A2, A83;
hence s = Sum p by A93, A84, RLVECT_1:def 12; :: thesis: verum