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: 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 A4: 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 A4;
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;
A5: 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 A5, 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
A6: for B being Element of Fin NAT holds S1[B,G . B] from FUNCT_2:sch 3(A3);
A7: 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 ;
A8: 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);
A9: rng (Sgm Y) = Y by FINSEQ_1:def 13;
dom (Sgm Y) = finSeg (card Y) by FINSEQ_3:40;
then dom ((Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y)) = Seg (card Y) by A8, A9, 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
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
A10: x in dom L and
A11: y = L . x by FUNCT_1:def 3;
x in dom (Sgm Y) by A10, FUNCT_1:11;
then A12: (Sgm Y) . x in Y by A9, FUNCT_1:def 3;
y = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . x) by A10, A11, FUNCT_1:12;
hence y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) by A8, A12, 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 set such that
A13: x in dom ((Sgm (dom (p | (B9 \/ {x})))) | Y) and
A14: y = ((Sgm (dom (p | (B9 \/ {x})))) | Y) . x by FUNCT_1:def 3;
A15: x in (dom (Sgm (dom (p | (B9 \/ {x}))))) /\ Y by A13, RELAT_1:61;
then A16: x in Y by XBOOLE_0:def 4;
then consider z being set such that
A17: z in dom (Sgm Y) and
A18: x = (Sgm Y) . z by A9, FUNCT_1:def 3;
x in dom (Sgm (dom (p | (B9 \/ {x})))) by A15, XBOOLE_0:def 4;
then A19: z in dom ((Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y)) by A17, A18, FUNCT_1:11;
then L . z = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . z) by FUNCT_1:12
.= y by A14, A16, A18, FUNCT_1:49 ;
hence y in rng L by A19, FUNCT_1:def 3; :: thesis: verum
end;
then A20: rng L = rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) by TARSKI:1;
x in {x} by TARSKI:def 1;
then A21: x in B9 \/ {x} by XBOOLE_0:def 3;
dom (p | (B9 \/ {x})) = (dom p) /\ (B9 \/ {x}) by RELAT_1:61;
then dom (p | (B9 \/ {x})) c= dom p by XBOOLE_1:17;
then A22: dom (p | (B9 \/ {x})) c= Seg (len p) by FINSEQ_1:def 3;
reconsider pB9x = p | (B9 \/ {x}) as FinSubsequence ;
rng (Sgm (dom (p | (B9 \/ {x})))) c= Seg (len p) by A22, FINSEQ_1:def 13;
then A23: 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:70;
then rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= dom p by A23, XBOOLE_1:1;
then A24: rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= Seg (len p) by FINSEQ_1:def 3;
reconsider pp = p | (B9 \/ {x}) as FinSubsequence ;
A25: dom (p | B9) = (dom p) /\ B9 by RELAT_1:61;
A26: 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
A27: 1 <= l and
A28: l < m and
A29: m <= len L and
A30: ( k1 = L . l & k2 = L . m ) ; :: thesis: k1 < k2
l <= len L by A28, A29, XXREAL_0:2;
then A31: l in dom L by A27, FINSEQ_3:25;
then A32: L . l = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . l) by FUNCT_1:12;
A33: (Sgm Y) . l in dom (Sgm (dom (p | (B9 \/ {x})))) by A31, FUNCT_1:11;
1 <= m by A27, A28, XXREAL_0:2;
then A34: m in dom L by A29, FINSEQ_3:25;
then A35: L . m = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . m) by FUNCT_1:12;
m in dom (Sgm Y) by A34, FUNCT_1:11;
then A36: m <= len (Sgm Y) by FINSEQ_3:25;
A37: (Sgm Y) . m in dom (Sgm (dom (p | (B9 \/ {x})))) by A34, 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 A33, A37;
A38: 1 <= K1 by A33, FINSEQ_3:25;
A39: K2 <= len (Sgm (dom (p | (B9 \/ {x})))) by A37, FINSEQ_3:25;
K1 < K2 by A27, A28, A36, FINSEQ_1:def 13;
hence k1 < k2 by A22, A30, A32, A35, A38, A39, FINSEQ_1:def 13; :: thesis: verum
end;
assume A40: 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 A41: 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 A40, XBOOLE_0:def 5;
then A42: {x} c= dom p by ZFMISC_1:31;
p . x = p /. x by A41, PARTFUN1:def 6;
then reconsider px = p . x as Element of K ;
A43: 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 A41, FINSEQ_1:38, ZFMISC_1:31;
then A44: dom (p * <*x*>) = dom <*px*> by A43, RELAT_1:27;
A45: now
let e be set ; :: thesis: ( e in dom <*px*> implies (p * <*x*>) . e = <*px*> . e )
assume A46: e in dom <*px*> ; :: thesis: (p * <*x*>) . e = <*px*> . e
then A47: e = 1 by A43, FINSEQ_1:2, TARSKI:def 1;
thus (p * <*x*>) . e = p . (<*x*> . e) by A44, A46, FUNCT_1:12
.= p . x by A47, FINSEQ_1:40
.= <*px*> . e by A47, FINSEQ_1:40 ; :: thesis: verum
end;
reconsider x9 = x as Element of D by A40, XBOOLE_0:def 5;
reconsider p9 = p as Function of D,E by FUNCT_2:1;
A48: E c= the carrier of K by FINSEQ_1:def 4;
not x in B9 by A40, XBOOLE_0:def 5;
then A49: not x in dom (p | B9) by A25, XBOOLE_0:def 4;
A50: rng (Sgm (dom pp)) = dom pp by FINSEQ_1:50;
then A51: rng (Sgm (dom (p | (B9 \/ {x})))) c= dom p by RELAT_1:60;
dom pp = (dom p) /\ (B9 \/ {x}) by RELAT_1:61;
then A52: x in rng (Sgm (dom (p | (B9 \/ {x})))) by A50, A41, A21, XBOOLE_0:def 4;
then rng ((Sgm (dom (p | (B9 \/ {x})))) |-- x) c= rng (Sgm (dom (p | (B9 \/ {x})))) by FINSEQ_4:44;
then A53: rng ((Sgm (dom (p | (B9 \/ {x})))) |-- x) c= D by A51, XBOOLE_1:1;
rng ((Sgm (dom (p | (B9 \/ {x})))) -| x) c= rng (Sgm (dom (p | (B9 \/ {x})))) by A52, FINSEQ_4:39;
then rng ((Sgm (dom (p | (B9 \/ {x})))) -| x) c= D by A51, XBOOLE_1:1;
then reconsider f39 = (Sgm (dom (p | (B9 \/ {x})))) -| x, f49 = (Sgm (dom (p | (B9 \/ {x})))) |-- x as FinSequence of D by A53, FINSEQ_1:def 4;
consider q2 being FinSequence of the carrier of K such that
A54: q2 = p * (Sgm (dom (p | (B9 \/ {x})))) and
A55: G . (B9 \/ {.x.}) = Sum q2 by A6;
reconsider p3 = p9 * f39, p4 = p9 * f49 as FinSequence of E ;
rng p3 c= E by FINSEQ_1:def 4;
then A56: rng p3 c= the carrier of K by A48, XBOOLE_1:1;
rng p4 c= E by FINSEQ_1:def 4;
then rng p4 c= the carrier of K by A48, XBOOLE_1:1;
then reconsider p3 = p3, p4 = p4 as FinSequence of the carrier of K by A56, FINSEQ_1:def 4;
consider q1 being FinSequence of the carrier of K such that
A57: q1 = p * (Sgm (dom (p | B9))) and
A58: G . B9 = Sum q1 by A6;
A59: Sgm (dom (p | (B9 \/ {x}))) is one-to-one by A22, 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 A42, XBOOLE_1:28
.= (dom (p | B9)) \ {x} by A25, XBOOLE_1:40
.= dom (p | B9) by A49, 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 A24, A20, A26, 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 A52, A59, FINSEQ_4:55 ;
then A60: q1 = p3 ^ p4 by A57, FINSEQOP:9;
q2 = p9 * ((f39 ^ <*x9*>) ^ f49) by A54, A52, FINSEQ_4:51
.= (p9 * (f39 ^ <*x9*>)) ^ (p9 * f49) by FINSEQOP:9
.= ((p9 * f39) ^ (p9 * <*x9*>)) ^ (p9 * f49) by FINSEQOP:9
.= (p3 ^ <*px*>) ^ p4 by A44, A45, FUNCT_1:2 ;
hence G . (B9 \/ {x}) = (Sum (p3 ^ <*px*>)) + (Sum p4) by A55, 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 A60, 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 A58, A41, SETWOP_2:20 ;
:: thesis: verum
end;
A61: 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
A62: q = p * (Sgm (dom (p | {x}))) and
A63: G . {.x.} = Sum q by A6;
A64: {} 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:50;
then (dom p) /\ {x} = {} by XBOOLE_0:def 7;
then q = p * (Sgm {}) by A62, RELAT_1:61
.= p * {} by A64, FINSEQ_1:51
.= <*> the carrier of K ;
hence G . {x} = 0. K by A63, RLVECT_1:43
.= the_unity_wrt the addF of K by Th9
.= ([#] (p,(the_unity_wrt the addF of K))) . x by A65, SETWOP_2:20 ;
:: 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 6;
then reconsider px = p . x as Element of K ;
A67: 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 A66, FINSEQ_1:38, ZFMISC_1:31;
then A68: dom (p * <*x*>) = dom <*px*> by A67, RELAT_1:27;
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:2, TARSKI:def 1;
thus (p * <*x*>) . e = p . (<*x*> . e) by A68, A70, FUNCT_1:12
.= p . x by A71, FINSEQ_1:40
.= <*px*> . e by A71, FINSEQ_1:40 ; :: thesis: verum
end;
A72: x <> 0 by A66, FINSEQ_3:25;
q = p * (Sgm ((dom p) /\ {x})) by A62, RELAT_1:61
.= p * (Sgm {x}) by A66, ZFMISC_1:46
.= p * <*x*> by A72, FINSEQ_3:44
.= <*px*> by A68, A69, FUNCT_1:2 ;
hence G . {x} = px by A63, RLVECT_1:44
.= ([#] (p,(the_unity_wrt the addF of K))) . x by A66, SETWOP_2:20 ;
:: 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:10;
A76: {} c= Seg 0 ;
consider q being FinSequence of the carrier of K such that
A77: q = p * (Sgm (dom (p | ({}. NAT)))) and
A78: G . ({}. NAT) = Sum q by A6;
q = p * (Sgm (dom {})) by A77
.= p * {} by A76, FINSEQ_1:51
.= <*> the carrier of K ;
hence e = G . {} by A78, A75, RLVECT_1:43; :: thesis: verum
end;
consider q1 being FinSequence of the carrier of K such that
A79: q1 = p * (Sgm (dom (p | (dom p)))) and
A80: G . (findom p) = Sum q1 by A6;
A81: the addF of K is having_a_unity by Th10;
q1 = p * (Sgm (dom p)) by A79, RELAT_1:69
.= 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 A2, A81, A80, A73, A61, A7, SETWISEO:def 3
.= the addF of K $$ p by Th10, SETWOP_2:def 2 ;
:: thesis: verum
end;
A82: p | (len p) = p | (Seg (len p)) by FINSEQ_1:def 15
.= p | (dom p) by FINSEQ_1:def 3
.= p by RELAT_1:69 ;
A83: 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
A84: j < len p and
A85: a = p . (j + 1) ; :: thesis: f . (j + 1) = (f . j) + a
A86: j + 1 <= len p by A84, NAT_1:13;
then A87: len (p | (j + 1)) = j + 1 by FINSEQ_1:59;
j <= j + 1 by NAT_1:11;
then A88: Seg j c= Seg (j + 1) by FINSEQ_1:5;
A89: p | j = p | (Seg j) by FINSEQ_1:def 15
.= (p | (Seg (j + 1))) | (Seg j) by A88, RELAT_1:74
.= (p | (j + 1)) | (Seg j) by FINSEQ_1:def 15 ;
A90: 1 <= j + 1 by NAT_1:11;
then A91: j + 1 in dom (p | (j + 1)) by A87, FINSEQ_3:25;
j + 1 in dom p by A86, A90, FINSEQ_3:25;
then a = p /. (j + 1) by A85, PARTFUN1:def 6
.= (p | (j + 1)) /. (j + 1) by A91, FINSEQ_4:70
.= (p | (j + 1)) . (j + 1) by A91, PARTFUN1:def 6 ;
then p | (j + 1) = (p | j) ^ <*a*> by A87, A89, FINSEQ_3:55;
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:4
.= (f . j) + a by A1 ;
:: thesis: verum
end;
p | 0 = <*> the carrier of K ;
then A92: f . 0 = the addF of K $$ (<*> the carrier of K) by A1
.= the_unity_wrt the addF of K by Th10, FINSOP_1:10
.= 0. K by Th9 ;
assume s = the addF of K $$ p ; :: thesis: s = Sum p
then s = f . (len p) by A1, A82;
hence s = Sum p by A92, A83, RLVECT_1:def 12; :: thesis: verum