let V be non empty Abelian add-associative right_zeroed addLoopStr ; for F, G being FinSequence of V st rng F = rng G & F is one-to-one & G is one-to-one holds
Sum F = Sum G
let F, G be FinSequence of V; ( rng F = rng G & F is one-to-one & G is one-to-one implies Sum F = Sum G )
defpred S1[ set ] means for H, I being FinSequence of V st len H = $1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I;
A1:
len F = len F
;
now for k being Nat st ( for H, I being FinSequence of V st len H = k & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I ) holds
for H, I being FinSequence of V st len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum Ilet k be
Nat;
( ( for H, I being FinSequence of V st len H = k & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I ) implies for H, I being FinSequence of V st len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I )assume A2:
for
H,
I being
FinSequence of
V st
len H = k &
rng H = rng I &
H is
one-to-one &
I is
one-to-one holds
Sum H = Sum I
;
for H, I being FinSequence of V st len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum Ilet H,
I be
FinSequence of
V;
( len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one implies Sum H = Sum I )assume that A3:
len H = k + 1
and A4:
rng H = rng I
and A5:
H is
one-to-one
and A6:
I is
one-to-one
;
Sum H = Sum I
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then A7:
k + 1
in dom H
by A3, FINSEQ_1:def 3;
then
H . (k + 1) in rng I
by A4, FUNCT_1:def 3;
then consider x being
object such that A8:
x in dom I
and A9:
H . (k + 1) = I . x
by FUNCT_1:def 3;
reconsider v =
H . (k + 1) as
Element of
V by A7, FUNCT_1:102;
reconsider n =
x as
Element of
NAT by A8;
A10:
len H = len I
by A4, A5, A6, FINSEQ_1:48;
then A11:
x in Seg (k + 1)
by A3, A8, FINSEQ_1:def 3;
then A12:
n <= k + 1
by FINSEQ_1:1;
then consider m2 being
Nat such that A13:
n + m2 = k + 1
by NAT_1:10;
defpred S2[
Nat,
object ]
means $2
= I . (n + $1);
reconsider m2 =
m2 as
Element of
NAT by ORDINAL1:def 12;
A14:
for
j being
Nat st
j in Seg m2 holds
ex
x being
object st
S2[
j,
x]
;
consider q2 being
FinSequence such that A15:
dom q2 = Seg m2
and A16:
for
k being
Nat st
k in Seg m2 holds
S2[
k,
q2 . k]
from FINSEQ_1:sch 1(A14);
A17:
rng q2 c= the
carrier of
V
proof
let x be
object ;
TARSKI:def 3 ( not x in rng q2 or x in the carrier of V )
assume
x in rng q2
;
x in the carrier of V
then consider y being
object such that A18:
y in dom q2
and A19:
x = q2 . y
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A18;
1
<= y
by A15, A18, FINSEQ_1:1;
then A20:
1
<= n + y
by NAT_1:12;
y <= m2
by A15, A18, FINSEQ_1:1;
then
n + y <= len I
by A3, A10, A13, XREAL_1:7;
then
n + y in dom I
by A20, FINSEQ_3:25;
then reconsider xx =
I . (n + y) as
Element of
V by FUNCT_1:102;
xx in the
carrier of
V
;
hence
x in the
carrier of
V
by A15, A16, A18, A19;
verum
end; reconsider p =
H | (Seg k) as
FinSequence of
V by FINSEQ_1:18;
A21:
p is
one-to-one
by A5, FUNCT_1:52;
Seg k = (Seg (k + 1)) \ {(k + 1)}
by FINSEQ_1:10;
then A22:
H .: (Seg k) = (H .: (Seg (k + 1))) \ (Im (H,(k + 1)))
by A5, FUNCT_1:64;
A23:
1
<= n
by A11, FINSEQ_1:1;
then consider m1 being
Nat such that A24:
1
+ m1 = n
by NAT_1:10;
reconsider q1 =
I | (Seg m1) as
FinSequence of
V by FINSEQ_1:18;
reconsider q2 =
q2 as
FinSequence of
V by A17, FINSEQ_1:def 4;
m1 <= n
by A24, NAT_1:11;
then A25:
m1 <= k + 1
by A12, XXREAL_0:2;
then A26:
len q1 = m1
by A3, A10, FINSEQ_1:17;
set q =
q1 ^ q2;
A29:
m1 < n
by A24, XREAL_1:29;
A30:
{v} misses rng (q1 ^ q2)
proof
set y = the
Element of
{v} /\ (rng (q1 ^ q2));
assume
not
{v} misses rng (q1 ^ q2)
;
contradiction
then A31:
{v} /\ (rng (q1 ^ q2)) <> {}
by XBOOLE_0:def 7;
then A32:
the
Element of
{v} /\ (rng (q1 ^ q2)) in {v}
by XBOOLE_0:def 4;
A33:
now not the Element of {v} /\ (rng (q1 ^ q2)) in rng q1assume
the
Element of
{v} /\ (rng (q1 ^ q2)) in rng q1
;
contradictionthen consider y1 being
object such that A34:
y1 in dom q1
and A35:
the
Element of
{v} /\ (rng (q1 ^ q2)) = q1 . y1
by FUNCT_1:def 3;
A36:
y1 in Seg m1
by A3, A10, A25, A34, FINSEQ_1:17;
reconsider y1 =
y1 as
Element of
NAT by A34;
y1 <= m1
by A36, FINSEQ_1:1;
then A37:
y1 <= k + 1
by A25, XXREAL_0:2;
1
<= y1
by A36, FINSEQ_1:1;
then
y1 in Seg (k + 1)
by A37, FINSEQ_1:1;
then A38:
y1 in dom I
by A3, A10, FINSEQ_1:def 3;
q1 . y1 = I . y1
by A34, FUNCT_1:47;
then A39:
I . y1 = I . n
by A9, A32, A35, TARSKI:def 1;
y1 <> n
by A29, A36, FINSEQ_1:1;
hence
contradiction
by A6, A8, A38, A39;
verum end;
A40:
the
Element of
{v} /\ (rng (q1 ^ q2)) = I . n
by A9, A32, TARSKI:def 1;
A41:
now not the Element of {v} /\ (rng (q1 ^ q2)) in rng q2assume
the
Element of
{v} /\ (rng (q1 ^ q2)) in rng q2
;
contradictionthen consider y1 being
object such that A42:
y1 in dom q2
and A43:
the
Element of
{v} /\ (rng (q1 ^ q2)) = q2 . y1
by FUNCT_1:def 3;
reconsider y1 =
y1 as
Element of
NAT by A42;
y1 <= m2
by A15, A42, FINSEQ_1:1;
then A44:
n + y1 <= k + 1
by A13, XREAL_1:7;
1
<= n + y1
by A23, NAT_1:12;
then
n + y1 in Seg (k + 1)
by A44, FINSEQ_1:1;
then A45:
n + y1 in dom I
by A3, A10, FINSEQ_1:def 3;
I . n = I . (n + y1)
by A15, A16, A40, A42, A43;
then A46:
n = n + y1
by A6, A8, A45;
y1 <> 0
by A15, A42, FINSEQ_1:1;
hence
contradiction
by A46;
verum end;
the
Element of
{v} /\ (rng (q1 ^ q2)) in rng (q1 ^ q2)
by A31, XBOOLE_0:def 4;
then
the
Element of
{v} /\ (rng (q1 ^ q2)) in (rng q1) \/ (rng q2)
by FINSEQ_1:31;
hence
contradiction
by A33, A41, XBOOLE_0:def 3;
verum
end; A47:
q1 ^ q2 is
one-to-one
proof
let y1,
y2 be
object ;
FUNCT_1:def 4 ( not y1 in dom (q1 ^ q2) or not y2 in dom (q1 ^ q2) or not (q1 ^ q2) . y1 = (q1 ^ q2) . y2 or y1 = y2 )
assume that A48:
(
y1 in dom (q1 ^ q2) &
y2 in dom (q1 ^ q2) )
and A49:
(q1 ^ q2) . y1 = (q1 ^ q2) . y2
;
y1 = y2
reconsider x1 =
y1,
x2 =
y2 as
Element of
NAT by A48;
A50:
now ( ex j1 being Nat st
( j1 in dom q2 & x1 = (len q1) + j1 ) & ex j2 being Nat st
( j2 in dom q2 & x2 = (len q1) + j2 ) implies y1 = y2 )given j1 being
Nat such that A51:
j1 in dom q2
and A52:
x1 = (len q1) + j1
;
( ex j2 being Nat st
( j2 in dom q2 & x2 = (len q1) + j2 ) implies y1 = y2 )A53:
q2 . j1 = I . (n + j1)
by A15, A16, A51;
j1 <= m2
by A15, A51, FINSEQ_1:1;
then A54:
n + j1 <= k + 1
by A13, XREAL_1:7;
1
<= n + j1
by A23, NAT_1:12;
then
n + j1 in Seg (k + 1)
by A54, FINSEQ_1:1;
then A55:
n + j1 in dom I
by A3, A10, FINSEQ_1:def 3;
given j2 being
Nat such that A56:
j2 in dom q2
and A57:
x2 = (len q1) + j2
;
y1 = y2A58:
q2 . j2 = I . (n + j2)
by A15, A16, A56;
j2 <= m2
by A15, A56, FINSEQ_1:1;
then A59:
n + j2 <= k + 1
by A13, XREAL_1:7;
1
<= n + j2
by A23, NAT_1:12;
then
n + j2 in Seg (k + 1)
by A59, FINSEQ_1:1;
then A60:
n + j2 in dom I
by A3, A10, FINSEQ_1:def 3;
q2 . j1 =
(q1 ^ q2) . (m1 + j2)
by A26, A49, A51, A52, A57, FINSEQ_1:def 7
.=
q2 . j2
by A26, A56, FINSEQ_1:def 7
;
then
n + j1 = n + j2
by A6, A53, A58, A55, A60;
hence
y1 = y2
by A52, A57;
verum end;
A61:
now ( x2 in dom q1 & ex j being Nat st
( j in dom q2 & x1 = (len q1) + j ) implies y1 = y2 )assume A62:
x2 in dom q1
;
( ex j being Nat st
( j in dom q2 & x1 = (len q1) + j ) implies y1 = y2 )then
q1 . x2 = I . x2
by FUNCT_1:47;
then A63:
(q1 ^ q2) . x2 = I . x2
by A62, FINSEQ_1:def 7;
A64:
x2 in Seg m1
by A3, A10, A25, A62, FINSEQ_1:17;
then A65:
1
<= x2
by FINSEQ_1:1;
A66:
x2 <= m1
by A64, FINSEQ_1:1;
then
x2 <= k + 1
by A25, XXREAL_0:2;
then
x2 in Seg (k + 1)
by A65, FINSEQ_1:1;
then A67:
x2 in dom I
by A3, A10, FINSEQ_1:def 3;
given j being
Nat such that A68:
j in dom q2
and A69:
x1 = (len q1) + j
;
y1 = y2
q2 . j = I . (n + j)
by A15, A16, A68;
then A70:
I . x2 = I . (n + j)
by A49, A68, A69, A63, FINSEQ_1:def 7;
j <= m2
by A15, A68, FINSEQ_1:1;
then A71:
n + j <= k + 1
by A13, XREAL_1:7;
1
<= n + j
by A23, NAT_1:12;
then
n + j in Seg (k + 1)
by A71, FINSEQ_1:1;
then A72:
n + j in dom I
by A3, A10, FINSEQ_1:def 3;
A73:
n <= n + j
by NAT_1:12;
x2 < n
by A29, A66, XXREAL_0:2;
hence
y1 = y2
by A6, A70, A67, A72, A73;
verum end;
A74:
now ( x1 in dom q1 & ex j being Nat st
( j in dom q2 & x2 = (len q1) + j ) implies y1 = y2 )assume A75:
x1 in dom q1
;
( ex j being Nat st
( j in dom q2 & x2 = (len q1) + j ) implies y1 = y2 )then
q1 . x1 = I . x1
by FUNCT_1:47;
then A76:
(q1 ^ q2) . x1 = I . x1
by A75, FINSEQ_1:def 7;
A77:
x1 in Seg m1
by A3, A10, A25, A75, FINSEQ_1:17;
then A78:
1
<= x1
by FINSEQ_1:1;
A79:
x1 <= m1
by A77, FINSEQ_1:1;
then
x1 <= k + 1
by A25, XXREAL_0:2;
then
x1 in Seg (k + 1)
by A78, FINSEQ_1:1;
then A80:
x1 in dom I
by A3, A10, FINSEQ_1:def 3;
given j being
Nat such that A81:
j in dom q2
and A82:
x2 = (len q1) + j
;
y1 = y2
q2 . j = I . (n + j)
by A15, A16, A81;
then A83:
I . x1 = I . (n + j)
by A49, A81, A82, A76, FINSEQ_1:def 7;
j <= m2
by A15, A81, FINSEQ_1:1;
then A84:
n + j <= k + 1
by A13, XREAL_1:7;
1
<= n + j
by A23, NAT_1:12;
then
n + j in Seg (k + 1)
by A84, FINSEQ_1:1;
then A85:
n + j in dom I
by A3, A10, FINSEQ_1:def 3;
A86:
n <= n + j
by NAT_1:12;
x1 < n
by A29, A79, XXREAL_0:2;
hence
y1 = y2
by A6, A83, A80, A85, A86;
verum end;
A87:
q1 is
one-to-one
by A6, FUNCT_1:52;
hence
y1 = y2
by A48, A74, A61, A50, FINSEQ_1:25;
verum
end;
k <= k + 1
by NAT_1:12;
then A89:
len p = k
by A3, FINSEQ_1:17;
len q2 = m2
by A15, FINSEQ_1:def 3;
then (len (q1 ^ <*v*>)) + (len q2) =
((len q1) + (len <*v*>)) + m2
by FINSEQ_1:22
.=
k + 1
by A24, A13, A26, FINSEQ_1:40
;
then
dom I = Seg ((len (q1 ^ <*v*>)) + (len q2))
by A3, A10, FINSEQ_1:def 3;
then A97:
I = (q1 ^ <*v*>) ^ q2
by A91, A27, FINSEQ_1:def 7;
then rng I =
(rng (q1 ^ <*v*>)) \/ (rng q2)
by FINSEQ_1:31
.=
((rng <*v*>) \/ (rng q1)) \/ (rng q2)
by FINSEQ_1:31
.=
({v} \/ (rng q1)) \/ (rng q2)
by FINSEQ_1:39
.=
{v} \/ ((rng q1) \/ (rng q2))
by XBOOLE_1:4
.=
{v} \/ (rng (q1 ^ q2))
by FINSEQ_1:31
;
then A98:
rng (q1 ^ q2) = (rng I) \ {v}
by A30, XBOOLE_1:88;
A99:
Seg (k + 1) = dom H
by A3, FINSEQ_1:def 3;
then
(
rng p = H .: (Seg k) &
rng H = H .: (Seg (k + 1)) )
by RELAT_1:113, RELAT_1:115;
then A100:
rng p = rng (q1 ^ q2)
by A4, A98, A99, A22, FINSEQ_1:4, FUNCT_1:59;
(
len <*v*> = 1 & ( for
k being
Nat st
k in dom p holds
H . k = p . k ) )
by FINSEQ_1:39, FUNCT_1:47;
then
H = p ^ <*v*>
by A89, A99, A90, FINSEQ_1:def 7;
then A101:
Sum H = (Sum p) + (Sum <*v*>)
by Th41;
Sum I =
(Sum (q1 ^ <*v*>)) + (Sum q2)
by A97, Th41
.=
((Sum q1) + (Sum <*v*>)) + (Sum q2)
by Th41
.=
(Sum <*v*>) + ((Sum q1) + (Sum q2))
by Def3
.=
(Sum (q1 ^ q2)) + (Sum <*v*>)
by Th41
;
hence
Sum H = Sum I
by A2, A89, A100, A21, A47, A101;
verum end;
then A102:
for k being Nat st S1[k] holds
S1[k + 1]
;
then A106:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A106, A102);
hence
( rng F = rng G & F is one-to-one & G is one-to-one implies Sum F = Sum G )
by A1; verum