:: AFINSQ_2 semantic presentation
begin
Lm1: for X, Y being finite set st X c= Y & card X = card Y holds
X = Y
proof
let X, Y be finite set ; ::_thesis: ( X c= Y & card X = card Y implies X = Y )
assume that
A1: X c= Y and
A2: card X = card Y ; ::_thesis: X = Y
card (Y \ X) = (card Y) - (card X) by A1, CARD_2:44;
then Y \ X = {} by A2;
then Y c= X by XBOOLE_1:37;
hence X = Y by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm2: for X, Y being finite set
for F being Function of X,Y st card X = card Y holds
( F is onto iff F is one-to-one )
proof
let X, Y be finite set ; ::_thesis: for F being Function of X,Y st card X = card Y holds
( F is onto iff F is one-to-one )
let F be Function of X,Y; ::_thesis: ( card X = card Y implies ( F is onto iff F is one-to-one ) )
assume A1: card X = card Y ; ::_thesis: ( F is onto iff F is one-to-one )
thus ( F is onto implies F is one-to-one ) ::_thesis: ( F is one-to-one implies F is onto )
proof
assume A2: F is onto ; ::_thesis: F is one-to-one
assume not F is one-to-one ; ::_thesis: contradiction
then consider x1, x2 being set such that
A3: x1 in dom F and
A4: x2 in dom F and
A5: F . x1 = F . x2 and
A6: x1 <> x2 by FUNCT_1:def_4;
reconsider Xx = X \ {x1} as finite set ;
Y c= F .: Xx
proof
let Fy be set ; :: according to TARSKI:def_3 ::_thesis: ( not Fy in Y or Fy in F .: Xx )
assume Fy in Y ; ::_thesis: Fy in F .: Xx
then Fy in rng F by A2, FUNCT_2:def_3;
then consider y being set such that
A7: y in dom F and
A8: F . y = Fy by FUNCT_1:def_3;
now__::_thesis:_Fy_in_F_.:_Xx
percases ( y = x1 or y <> x1 ) ;
supposeA9: y = x1 ; ::_thesis: Fy in F .: Xx
x2 in Xx by A4, A6, ZFMISC_1:56;
hence Fy in F .: Xx by A4, A5, A8, A9, FUNCT_1:def_6; ::_thesis: verum
end;
suppose y <> x1 ; ::_thesis: Fy in F .: Xx
then y in Xx by A7, ZFMISC_1:56;
hence Fy in F .: Xx by A7, A8, FUNCT_1:def_6; ::_thesis: verum
end;
end;
end;
hence Fy in F .: Xx ; ::_thesis: verum
end;
then A10: card Y c= card Xx by CARD_1:66;
{x1} meets X by A3, ZFMISC_1:48;
then A11: Xx <> X by XBOOLE_1:83;
Xx c< X by A11, XBOOLE_0:def_8;
then card Xx < card X by CARD_2:48;
hence contradiction by A1, A10, NAT_1:39; ::_thesis: verum
end;
thus ( F is one-to-one implies F is onto ) ::_thesis: verum
proof
assume F is one-to-one ; ::_thesis: F is onto
then dom F,F .: (dom F) are_equipotent by CARD_1:33;
then A12: card (dom F) = card (F .: (dom F)) by CARD_1:5;
assume not F is onto ; ::_thesis: contradiction
then not rng F = Y by FUNCT_2:def_3;
then not Y c= rng F by XBOOLE_0:def_10;
then consider y being set such that
A13: y in Y and
A14: not y in rng F by TARSKI:def_3;
A15: card (rng F) <= card (Y \ {y}) by A14, NAT_1:43, ZFMISC_1:34;
A16: F .: (dom F) = rng F by RELAT_1:113;
{y} meets Y by A13, ZFMISC_1:48;
then A17: Y \ {y} <> Y by XBOOLE_1:83;
Y \ {y} c< Y by A17, XBOOLE_0:def_8;
then card (Y \ {y}) < card Y by CARD_2:48;
hence contradiction by A1, A13, A15, A12, A16, FUNCT_2:def_1; ::_thesis: verum
end;
end;
theorem Th1: :: AFINSQ_2:1
for i being Nat
for x being set st x in i holds
x is Element of NAT
proof
let i be Nat; ::_thesis: for x being set st x in i holds
x is Element of NAT
let x be set ; ::_thesis: ( x in i implies x is Element of NAT )
A1: i c= NAT ;
assume x in i ; ::_thesis: x is Element of NAT
hence x is Element of NAT by A1; ::_thesis: verum
end;
registration
cluster natural -> natural-membered for set ;
coherence
for b1 being Nat holds b1 is natural-membered
proof
let n be Nat; ::_thesis: n is natural-membered
for x being set st x in n holds
x is natural by Th1;
hence n is natural-membered by MEMBERED:def_6; ::_thesis: verum
end;
end;
begin
theorem Th2: :: AFINSQ_2:2
for X0 being finite natural-membered set ex n being Nat st X0 c= n
proof
let X0 be finite natural-membered set ; ::_thesis: ex n being Nat st X0 c= n
consider p being Function such that
A1: rng p = X0 and
A2: dom p in NAT by FINSET_1:def_1;
reconsider np = dom p as Element of NAT by A2;
np = dom p ;
then reconsider p = p as XFinSequence by AFINSQ_1:5;
X0 c= NAT by MEMBERED:6;
then reconsider p = p as XFinSequence of NAT by A1, RELAT_1:def_19;
defpred S1[ Nat] means ex n being Nat st
for i being Nat st i in $1 & $1 -' 1 in dom p holds
p . i in n;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
then consider n being Nat such that
A4: for i being Nat st i in k & k -' 1 in dom p holds
p . i in n ;
percases ( (k + 1) - 1 < len p or (k + 1) - 1 >= len p ) ;
supposeA5: (k + 1) - 1 < len p ; ::_thesis: S1[k + 1]
set m = p . k;
set m2 = max (n,((p . k) + 1));
k -' 1 <= k by NAT_D:35;
then k -' 1 < len p by A5, XXREAL_0:2;
then A6: k -' 1 in dom p by NAT_1:44;
for i being Nat st i in k + 1 & (k + 1) -' 1 in dom p holds
p . i in max (n,((p . k) + 1))
proof
let i be Nat; ::_thesis: ( i in k + 1 & (k + 1) -' 1 in dom p implies p . i in max (n,((p . k) + 1)) )
assume that
A7: i in k + 1 and
(k + 1) -' 1 in dom p ; ::_thesis: p . i in max (n,((p . k) + 1))
A8: i < k + 1 by A7, NAT_1:44;
percases ( i < k or i >= k ) ;
supposeA9: i < k ; ::_thesis: p . i in max (n,((p . k) + 1))
set k0 = p . i;
i in k by A9, NAT_1:44;
then p . i in n by A4, A6;
then p . i < n by NAT_1:44;
then p . i < max (n,((p . k) + 1)) by XXREAL_0:30;
hence p . i in max (n,((p . k) + 1)) by NAT_1:44; ::_thesis: verum
end;
supposeA10: i >= k ; ::_thesis: p . i in max (n,((p . k) + 1))
p . k < (p . k) + 1 by XREAL_1:29;
then A11: p . k < max (n,((p . k) + 1)) by XXREAL_0:30;
i <= k by A8, NAT_1:13;
then p . i = p . k by A10, XXREAL_0:1;
hence p . i in max (n,((p . k) + 1)) by A11, NAT_1:44; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
supposeA12: (k + 1) - 1 >= len p ; ::_thesis: S1[k + 1]
(k + 1) -' 1 = k by NAT_D:34;
then for i being Nat st i in k + 1 & (k + 1) -' 1 in dom p holds
p . i in 2 by A12, NAT_1:44;
hence S1[k + 1] ; ::_thesis: verum
end;
end;
end;
for i being Nat st i in 0 & 0 -' 1 in dom p holds
p . i in 0 ;
then A13: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A13, A3);
then consider n being Nat such that
A14: for i being Nat st i in len p & (len p) -' 1 in dom p holds
p . i in n ;
rng p c= n
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in n )
assume y in rng p ; ::_thesis: y in n
then consider x being set such that
A15: x in dom p and
A16: y = p . x by FUNCT_1:def_3;
A17: (len p) - 1 < len p by XREAL_1:44;
0 + 1 <= len p by A15, NAT_1:13;
then (len p) -' 1 = (len p) - 1 by XREAL_1:233;
then (len p) -' 1 in dom p by A17, NAT_1:44;
hence y in n by A14, A15, A16; ::_thesis: verum
end;
hence ex n being Nat st X0 c= n by A1; ::_thesis: verum
end;
theorem Th3: :: AFINSQ_2:3
for x being set
for p being XFinSequence st x in rng p holds
ex i being Element of NAT st
( i in dom p & p . i = x )
proof
let x be set ; ::_thesis: for p being XFinSequence st x in rng p holds
ex i being Element of NAT st
( i in dom p & p . i = x )
let p be XFinSequence; ::_thesis: ( x in rng p implies ex i being Element of NAT st
( i in dom p & p . i = x ) )
assume x in rng p ; ::_thesis: ex i being Element of NAT st
( i in dom p & p . i = x )
then ex a being set st
( a in dom p & x = p . a ) by FUNCT_1:def_3;
hence ex i being Element of NAT st
( i in dom p & p . i = x ) ; ::_thesis: verum
end;
theorem Th4: :: AFINSQ_2:4
for D being set
for p being XFinSequence st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is XFinSequence of D
proof
let D be set ; ::_thesis: for p being XFinSequence st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is XFinSequence of D
let p be XFinSequence; ::_thesis: ( ( for i being Nat st i in dom p holds
p . i in D ) implies p is XFinSequence of D )
assume A1: for i being Nat st i in dom p holds
p . i in D ; ::_thesis: p is XFinSequence of D
rng p c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in D )
assume x in rng p ; ::_thesis: x in D
then ex i being Element of NAT st
( i in dom p & p . i = x ) by Th3;
hence x in D by A1; ::_thesis: verum
end;
hence p is XFinSequence of D by RELAT_1:def_19; ::_thesis: verum
end;
scheme :: AFINSQ_2:sch 1
XSeqLambdaD{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } :
ex p being XFinSequence of F2() st
( len p = F1() & ( for j being Nat st j in F1() holds
p . j = F3(j) ) )
proof
consider z being XFinSequence such that
A1: len z = F1() and
A2: for i being Nat st i in F1() holds
z . i = F3(i) from AFINSQ_1:sch_2();
for j being Nat st j in F1() holds
z . j in F2()
proof
let j be Nat; ::_thesis: ( j in F1() implies z . j in F2() )
reconsider j0 = j as Element of NAT by ORDINAL1:def_12;
assume j in F1() ; ::_thesis: z . j in F2()
then z . j0 = F3(j0) by A2;
hence z . j in F2() ; ::_thesis: verum
end;
then reconsider z = z as XFinSequence of F2() by A1, Th4;
take z ; ::_thesis: ( len z = F1() & ( for j being Nat st j in F1() holds
z . j = F3(j) ) )
thus len z = F1() by A1; ::_thesis: for j being Nat st j in F1() holds
z . j = F3(j)
let j be Nat; ::_thesis: ( j in F1() implies z . j = F3(j) )
thus ( j in F1() implies z . j = F3(j) ) by A2; ::_thesis: verum
end;
registration
cluster Relation-like NAT -defined Function-like empty T-Sequence-like natural-valued finite V86() for set ;
existence
ex b1 being XFinSequence st
( b1 is empty & b1 is natural-valued )
proof
take the empty XFinSequence of NAT ; ::_thesis: ( the empty XFinSequence of NAT is empty & the empty XFinSequence of NAT is natural-valued )
thus ( the empty XFinSequence of NAT is empty & the empty XFinSequence of NAT is natural-valued ) ; ::_thesis: verum
end;
let p be T-Sequence-like complex-valued Function;
cluster - p -> T-Sequence-like ;
coherence
- p is T-Sequence-like
proof
( dom p = dom (- p) & dom p is ordinal ) by VALUED_1:8;
hence - p is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
clusterp " -> T-Sequence-like ;
coherence
p " is T-Sequence-like
proof
dom p = dom (p ") by VALUED_1:def_7;
hence p " is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
clusterp ^2 -> T-Sequence-like ;
coherence
p ^2 is T-Sequence-like
proof
dom p = dom (p ^2) by VALUED_1:11;
hence p ^2 is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
cluster|.p.| -> T-Sequence-like ;
coherence
abs p is T-Sequence-like
proof
dom p = dom (abs p) by VALUED_1:def_11;
hence abs p is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
let q be T-Sequence-like complex-valued Function;
clusterp + q -> T-Sequence-like ;
coherence
p + q is T-Sequence-like
proof
( dom (p + q) = (dom p) /\ (dom q) & dom p is ordinal & dom q is ordinal ) by VALUED_1:def_1;
hence p + q is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
clusterp - q -> T-Sequence-like ;
coherence
p - q is T-Sequence-like ;
clusterp (#) q -> T-Sequence-like ;
coherence
p (#) q is T-Sequence-like
proof
( dom (p (#) q) = (dom p) /\ (dom q) & dom p is ordinal & dom q is ordinal ) by VALUED_1:def_4;
hence p (#) q is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
clusterp /" q -> T-Sequence-like ;
coherence
p /" q is T-Sequence-like ;
end;
registration
let p be complex-valued finite Function;
cluster - p -> finite ;
coherence
- p is finite
proof
dom p = dom (- p) by VALUED_1:8;
hence - p is finite by FINSET_1:10; ::_thesis: verum
end;
clusterp " -> finite ;
coherence
p " is finite
proof
dom p = dom (p ") by VALUED_1:def_7;
hence p " is finite by FINSET_1:10; ::_thesis: verum
end;
clusterp ^2 -> finite ;
coherence
p ^2 is finite
proof
dom p = dom (p ^2) by VALUED_1:11;
hence p ^2 is finite by FINSET_1:10; ::_thesis: verum
end;
cluster|.p.| -> finite ;
coherence
abs p is finite
proof
dom p = dom (abs p) by VALUED_1:def_11;
hence abs p is finite by FINSET_1:10; ::_thesis: verum
end;
let q be complex-valued Function;
clusterp + q -> finite ;
coherence
p + q is finite
proof
dom (p + q) = (dom p) /\ (dom q) by VALUED_1:def_1;
hence p + q is finite by FINSET_1:10; ::_thesis: verum
end;
clusterp - q -> finite ;
coherence
p - q is finite ;
clusterp (#) q -> finite ;
coherence
p (#) q is finite
proof
dom (p (#) q) = (dom p) /\ (dom q) by VALUED_1:def_4;
hence p (#) q is finite by FINSET_1:10; ::_thesis: verum
end;
clusterp /" q -> finite ;
coherence
p /" q is finite ;
clusterq /" p -> finite ;
coherence
q /" p is finite ;
end;
registration
let p be T-Sequence-like complex-valued Function;
let c be complex number ;
clusterc + p -> T-Sequence-like ;
coherence
c + p is T-Sequence-like
proof
dom p = dom (c + p) by VALUED_1:def_2;
hence c + p is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
clusterp - c -> T-Sequence-like ;
coherence
p - c is T-Sequence-like ;
clusterc (#) p -> T-Sequence-like ;
coherence
c (#) p is T-Sequence-like
proof
dom p = dom (c (#) p) by VALUED_1:def_5;
hence c (#) p is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
end;
registration
let p be complex-valued finite Function;
let c be complex number ;
clusterc + p -> finite ;
coherence
c + p is finite
proof
dom p = dom (c + p) by VALUED_1:def_2;
hence c + p is finite by FINSET_1:10; ::_thesis: verum
end;
clusterp - c -> finite ;
coherence
p - c is finite ;
clusterc (#) p -> finite ;
coherence
c (#) p is finite
proof
dom p = dom (c (#) p) by VALUED_1:def_5;
hence c (#) p is finite by FINSET_1:10; ::_thesis: verum
end;
end;
definition
let p be XFinSequence;
func Rev p -> XFinSequence means :Def1: :: AFINSQ_2:def 1
( len it = len p & ( for i being Nat st i in dom it holds
it . i = p . ((len p) - (i + 1)) ) );
existence
ex b1 being XFinSequence st
( len b1 = len p & ( for i being Nat st i in dom b1 holds
b1 . i = p . ((len p) - (i + 1)) ) )
proof
deffunc H1( Nat) -> set = p . ((len p) - ($1 + 1));
ex q being XFinSequence st
( len q = len p & ( for k being Nat st k in len p holds
q . k = H1(k) ) ) from AFINSQ_1:sch_2();
hence ex b1 being XFinSequence st
( len b1 = len p & ( for i being Nat st i in dom b1 holds
b1 . i = p . ((len p) - (i + 1)) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being XFinSequence st len b1 = len p & ( for i being Nat st i in dom b1 holds
b1 . i = p . ((len p) - (i + 1)) ) & len b2 = len p & ( for i being Nat st i in dom b2 holds
b2 . i = p . ((len p) - (i + 1)) ) holds
b1 = b2
proof
let f1, f2 be XFinSequence; ::_thesis: ( len f1 = len p & ( for i being Nat st i in dom f1 holds
f1 . i = p . ((len p) - (i + 1)) ) & len f2 = len p & ( for i being Nat st i in dom f2 holds
f2 . i = p . ((len p) - (i + 1)) ) implies f1 = f2 )
assume that
A1: len f1 = len p and
A2: for i being Nat st i in dom f1 holds
f1 . i = p . ((len p) - (i + 1)) and
A3: len f2 = len p and
A4: for i being Nat st i in dom f2 holds
f2 . i = p . ((len p) - (i + 1)) ; ::_thesis: f1 = f2
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
f1_._i_=_f2_._i
let i be Nat; ::_thesis: ( i in dom p implies f1 . i = f2 . i )
assume A5: i in dom p ; ::_thesis: f1 . i = f2 . i
then f1 . i = p . ((len p) - (i + 1)) by A1, A2;
hence f1 . i = f2 . i by A3, A4, A5; ::_thesis: verum
end;
hence f1 = f2 by A1, A3, AFINSQ_1:8; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Rev AFINSQ_2:def_1_:_
for p, b2 being XFinSequence holds
( b2 = Rev p iff ( len b2 = len p & ( for i being Nat st i in dom b2 holds
b2 . i = p . ((len p) - (i + 1)) ) ) );
theorem Th5: :: AFINSQ_2:5
for p being XFinSequence holds
( dom p = dom (Rev p) & rng p = rng (Rev p) )
proof
let p be XFinSequence; ::_thesis: ( dom p = dom (Rev p) & rng p = rng (Rev p) )
thus A1: dom p = len p
.= len (Rev p) by Def1
.= dom (Rev p) ; ::_thesis: rng p = rng (Rev p)
A2: len p = len (Rev p) by Def1;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: rng (Rev p) c= rng p
let x be set ; ::_thesis: ( x in rng p implies x in rng (Rev p) )
assume x in rng p ; ::_thesis: x in rng (Rev p)
then consider z being set such that
A3: z in dom p and
A4: p . z = x by FUNCT_1:def_3;
reconsider i = z as Element of NAT by A3;
i < len p by A3, NAT_1:44;
then i + 1 <= len p by NAT_1:13;
then (len p) -' (i + 1) = (len p) - (i + 1) by XREAL_1:233;
then reconsider j = (len p) - (i + 1) as Element of NAT ;
(len p) - (i + 1) < len p by XREAL_1:44;
then A5: j in len (Rev p) by A2, NAT_1:44;
then (Rev p) . j = p . ((len p) - (j + 1)) by Def1;
hence x in rng (Rev p) by A4, A5, FUNCT_1:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Rev p) or x in rng p )
assume x in rng (Rev p) ; ::_thesis: x in rng p
then consider z being set such that
A6: z in dom (Rev p) and
A7: (Rev p) . z = x by FUNCT_1:def_3;
reconsider i = z as Element of NAT by A6;
i < len p by A2, A6, NAT_1:44;
then i + 1 <= len p by NAT_1:13;
then (len p) -' (i + 1) = (len p) - (i + 1) by XREAL_1:233;
then reconsider j = (len p) - (i + 1) as Element of NAT ;
(len p) - (i + 1) < len p by XREAL_1:44;
then A8: j in len (Rev p) by A2, NAT_1:44;
(Rev p) . i = p . ((len p) - (i + 1)) by A6, Def1;
hence x in rng p by A1, A7, A8, FUNCT_1:def_3; ::_thesis: verum
end;
registration
let D be set ;
let f be XFinSequence of D;
cluster Rev f -> D -valued ;
coherence
Rev f is D -valued
proof
rng f = rng (Rev f) by Th5;
hence Rev f is D -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
definition
let p be XFinSequence;
let n be Nat;
funcp /^ n -> XFinSequence means :Def2: :: AFINSQ_2:def 2
( len it = (len p) -' n & ( for m being Nat st m in dom it holds
it . m = p . (m + n) ) );
existence
ex b1 being XFinSequence st
( len b1 = (len p) -' n & ( for m being Nat st m in dom b1 holds
b1 . m = p . (m + n) ) )
proof
thus ex p1 being XFinSequence st
( len p1 = (len p) -' n & ( for m being Nat st m in dom p1 holds
p1 . m = p . (m + n) ) ) ::_thesis: verum
proof
deffunc H1( Nat) -> set = p . ($1 + n);
set k = (len p) -' n;
consider q being XFinSequence such that
A1: ( len q = (len p) -' n & ( for m2 being Nat st m2 in (len p) -' n holds
q . m2 = H1(m2) ) ) from AFINSQ_1:sch_2();
take q ; ::_thesis: ( len q = (len p) -' n & ( for m being Nat st m in dom q holds
q . m = p . (m + n) ) )
thus ( len q = (len p) -' n & ( for m being Nat st m in dom q holds
q . m = p . (m + n) ) ) by A1; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being XFinSequence st len b1 = (len p) -' n & ( for m being Nat st m in dom b1 holds
b1 . m = p . (m + n) ) & len b2 = (len p) -' n & ( for m being Nat st m in dom b2 holds
b2 . m = p . (m + n) ) holds
b1 = b2
proof
let p1, p2 be XFinSequence; ::_thesis: ( len p1 = (len p) -' n & ( for m being Nat st m in dom p1 holds
p1 . m = p . (m + n) ) & len p2 = (len p) -' n & ( for m being Nat st m in dom p2 holds
p2 . m = p . (m + n) ) implies p1 = p2 )
thus ( len p1 = (len p) -' n & ( for m being Nat st m in dom p1 holds
p1 . m = p . (m + n) ) & len p2 = (len p) -' n & ( for m being Nat st m in dom p2 holds
p2 . m = p . (m + n) ) implies p1 = p2 ) ::_thesis: verum
proof
assume that
A2: len p1 = (len p) -' n and
A3: for m being Nat st m in dom p1 holds
p1 . m = p . (m + n) and
A4: len p2 = (len p) -' n and
A5: for m being Nat st m in dom p2 holds
p2 . m = p . (m + n) ; ::_thesis: p1 = p2
now__::_thesis:_for_m_being_Nat_st_m_in_dom_p1_holds_
p1_._m_=_p2_._m
let m be Nat; ::_thesis: ( m in dom p1 implies p1 . m = p2 . m )
assume A6: m in dom p1 ; ::_thesis: p1 . m = p2 . m
then p1 . m = p . (m + n) by A3;
hence p1 . m = p2 . m by A2, A4, A5, A6; ::_thesis: verum
end;
hence p1 = p2 by A2, A4, AFINSQ_1:8; ::_thesis: verum
end;
end;
end;
:: deftheorem Def2 defines /^ AFINSQ_2:def_2_:_
for p being XFinSequence
for n being Nat
for b3 being XFinSequence holds
( b3 = p /^ n iff ( len b3 = (len p) -' n & ( for m being Nat st m in dom b3 holds
b3 . m = p . (m + n) ) ) );
theorem Th6: :: AFINSQ_2:6
for n being Nat
for p being XFinSequence st n >= len p holds
p /^ n = {}
proof
let n be Nat; ::_thesis: for p being XFinSequence st n >= len p holds
p /^ n = {}
let p be XFinSequence; ::_thesis: ( n >= len p implies p /^ n = {} )
assume n >= len p ; ::_thesis: p /^ n = {}
then (len p) -' n = 0 by NAT_2:8;
then len (p /^ n) = 0 by Def2;
hence p /^ n = {} ; ::_thesis: verum
end;
theorem Th7: :: AFINSQ_2:7
for n being Nat
for p being XFinSequence st n < len p holds
len (p /^ n) = (len p) - n
proof
let n be Nat; ::_thesis: for p being XFinSequence st n < len p holds
len (p /^ n) = (len p) - n
let p be XFinSequence; ::_thesis: ( n < len p implies len (p /^ n) = (len p) - n )
assume n < len p ; ::_thesis: len (p /^ n) = (len p) - n
then (len p) - n >= 0 by XREAL_1:48;
then (len p) -' n = (len p) - n by XREAL_0:def_2;
hence len (p /^ n) = (len p) - n by Def2; ::_thesis: verum
end;
theorem Th8: :: AFINSQ_2:8
for m, n being Nat
for p being XFinSequence st m + n < len p holds
(p /^ n) . m = p . (m + n)
proof
let m, n be Nat; ::_thesis: for p being XFinSequence st m + n < len p holds
(p /^ n) . m = p . (m + n)
let p be XFinSequence; ::_thesis: ( m + n < len p implies (p /^ n) . m = p . (m + n) )
assume A1: m + n < len p ; ::_thesis: (p /^ n) . m = p . (m + n)
then A2: m < (len p) - n by XREAL_1:20;
len (p /^ n) = (len p) - n by A1, Th7, NAT_1:12;
then m in dom (p /^ n) by A2, NAT_1:44;
hence (p /^ n) . m = p . (m + n) by Def2; ::_thesis: verum
end;
registration
let f be one-to-one XFinSequence;
let n be Nat;
clusterf /^ n -> one-to-one ;
coherence
f /^ n is one-to-one
proof
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom (f /^ n) or not y in dom (f /^ n) or not (f /^ n) . x = (f /^ n) . y or x = y )
assume that
A1: x in dom (f /^ n) and
A2: y in dom (f /^ n) and
A3: (f /^ n) . x = (f /^ n) . y ; ::_thesis: x = y
reconsider nx = x, ny = y as Nat by A1, A2;
A4: nx < len (f /^ n) by A1, NAT_1:44;
A5: len (f /^ n) = (len f) -' n by Def2;
A6: ny < len (f /^ n) by A2, NAT_1:44;
percases ( n <= len f or n > len f ) ;
suppose n <= len f ; ::_thesis: x = y
then A7: (len f) -' n = (len f) - n by XREAL_1:233;
then A8: nx + n < len f by A4, A5, XREAL_1:20;
then A9: nx + n in dom f by NAT_1:44;
A10: ny + n < len f by A6, A5, A7, XREAL_1:20;
then A11: ny + n in dom f by NAT_1:44;
A12: (f /^ n) . ny = f . (ny + n) by A10, Th8;
(f /^ n) . nx = f . (nx + n) by A8, Th8;
then nx + n = ny + n by A3, A9, A12, A11, FUNCT_1:def_4;
hence x = y ; ::_thesis: verum
end;
suppose n > len f ; ::_thesis: x = y
then f /^ n = {} by Th6;
hence x = y by A1; ::_thesis: verum
end;
end;
end;
end;
theorem Th9: :: AFINSQ_2:9
for n being Nat
for p being XFinSequence holds rng (p /^ n) c= rng p
proof
let n be Nat; ::_thesis: for p being XFinSequence holds rng (p /^ n) c= rng p
let p be XFinSequence; ::_thesis: rng (p /^ n) c= rng p
thus rng (p /^ n) c= rng p ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (p /^ n) or z in rng p )
assume z in rng (p /^ n) ; ::_thesis: z in rng p
then consider x being set such that
A1: x in dom (p /^ n) and
A2: z = (p /^ n) . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A1;
nx < len (p /^ n) by A1, NAT_1:44;
then A3: nx < (len p) -' n by Def2;
percases ( n < len p or n >= len p ) ;
suppose n < len p ; ::_thesis: z in rng p
then (len p) -' n = (len p) - n by XREAL_1:233;
then nx + n < len p by A3, XREAL_1:20;
then A4: nx + n in dom p by NAT_1:44;
(p /^ n) . nx = p . (nx + n) by A1, Def2;
hence z in rng p by A2, A4, FUNCT_1:def_3; ::_thesis: verum
end;
suppose n >= len p ; ::_thesis: z in rng p
then p /^ n = {} by Th6;
hence z in rng p by A1; ::_thesis: verum
end;
end;
end;
end;
theorem Th10: :: AFINSQ_2:10
for p being XFinSequence holds p /^ 0 = p
proof
let p be XFinSequence; ::_thesis: p /^ 0 = p
percases ( 0 < len p or 0 >= len p ) ;
supposeA1: 0 < len p ; ::_thesis: p /^ 0 = p
A2: now__::_thesis:_for_i_being_Nat_st_i_<_len_(p_/^_0)_holds_
(p_/^_0)_._i_=_p_._i
let i be Nat; ::_thesis: ( i < len (p /^ 0) implies (p /^ 0) . i = p . i )
assume i < len (p /^ 0) ; ::_thesis: (p /^ 0) . i = p . i
then i in dom (p /^ 0) by NAT_1:44;
hence (p /^ 0) . i = p . (i + 0) by Def2
.= p . i ;
::_thesis: verum
end;
len (p /^ 0) = (len p) - 0 by A1, Th7
.= len p ;
hence p /^ 0 = p by A2, AFINSQ_1:9; ::_thesis: verum
end;
supposeA3: 0 >= len p ; ::_thesis: p /^ 0 = p
then p /^ 0 = {} by Th6;
hence p /^ 0 = p by A3; ::_thesis: verum
end;
end;
end;
theorem Th11: :: AFINSQ_2:11
for i being Nat
for p, q being XFinSequence holds (p ^ q) /^ ((len p) + i) = q /^ i
proof
let i be Nat; ::_thesis: for p, q being XFinSequence holds (p ^ q) /^ ((len p) + i) = q /^ i
let p, q be XFinSequence; ::_thesis: (p ^ q) /^ ((len p) + i) = q /^ i
A1: len (p ^ q) = (len p) + (len q) by AFINSQ_1:17;
percases ( i < len q or i >= len q ) ;
supposeA2: i < len q ; ::_thesis: (p ^ q) /^ ((len p) + i) = q /^ i
then (len p) + i < (len p) + (len q) by XREAL_1:6;
then (len p) + i < len (p ^ q) by AFINSQ_1:17;
then A3: len ((p ^ q) /^ ((len p) + i)) = (len (p ^ q)) - ((len p) + i) by Th7
.= ((len q) + (len p)) - ((len p) + i) by AFINSQ_1:17
.= (len q) - i
.= len (q /^ i) by A2, Th7 ;
now__::_thesis:_for_k_being_Nat_st_k_<_len_(q_/^_i)_holds_
((p_^_q)_/^_((len_p)_+_i))_._k_=_(q_/^_i)_._k
let k be Nat; ::_thesis: ( k < len (q /^ i) implies ((p ^ q) /^ ((len p) + i)) . k = (q /^ i) . k )
assume A4: k < len (q /^ i) ; ::_thesis: ((p ^ q) /^ ((len p) + i)) . k = (q /^ i) . k
then A5: k in dom (q /^ i) by NAT_1:44;
k < (len q) - i by A2, A4, Th7;
then i + k < len q by XREAL_1:20;
then A6: i + k in dom q by NAT_1:44;
k in dom ((p ^ q) /^ ((len p) + i)) by A3, A4, NAT_1:44;
hence ((p ^ q) /^ ((len p) + i)) . k = (p ^ q) . (((len p) + i) + k) by Def2
.= (p ^ q) . ((len p) + (i + k))
.= q . (i + k) by A6, AFINSQ_1:def_3
.= (q /^ i) . k by A5, Def2 ;
::_thesis: verum
end;
hence (p ^ q) /^ ((len p) + i) = q /^ i by A3, AFINSQ_1:9; ::_thesis: verum
end;
supposeA7: i >= len q ; ::_thesis: (p ^ q) /^ ((len p) + i) = q /^ i
then (len p) + i >= len (p ^ q) by A1, XREAL_1:6;
hence (p ^ q) /^ ((len p) + i) = {} by Th6
.= q /^ i by A7, Th6 ;
::_thesis: verum
end;
end;
end;
theorem Th12: :: AFINSQ_2:12
for p, q being XFinSequence holds (p ^ q) /^ (len p) = q
proof
let p, q be XFinSequence; ::_thesis: (p ^ q) /^ (len p) = q
thus (p ^ q) /^ (len p) = (p ^ q) /^ ((len p) + 0)
.= q /^ 0 by Th11
.= q by Th10 ; ::_thesis: verum
end;
theorem :: AFINSQ_2:13
for n being Nat
for p being XFinSequence holds (p | n) ^ (p /^ n) = p
proof
let n be Nat; ::_thesis: for p being XFinSequence holds (p | n) ^ (p /^ n) = p
let p be XFinSequence; ::_thesis: (p | n) ^ (p /^ n) = p
set pn = p /^ n;
now__::_thesis:_(_(_len_p_<=_n_&_(p_|_n)_^_(p_/^_n)_=_p_)_or_(_n_<_len_p_&_(p_|_n)_^_(p_/^_n)_=_p_)_)
percases ( len p <= n or n < len p ) ;
caseA1: len p <= n ; ::_thesis: (p | n) ^ (p /^ n) = p
A2: p ^ {} = p ;
p /^ n = {} by A1, Th6;
hence (p | n) ^ (p /^ n) = p by A1, A2, AFINSQ_1:52; ::_thesis: verum
end;
caseA3: n < len p ; ::_thesis: (p | n) ^ (p /^ n) = p
set g = p | n;
A4: len (p | n) = n by A3, AFINSQ_1:54;
A5: len (p /^ n) = (len p) - n by A3, Th7;
A6: now__::_thesis:_for_m_being_Nat_st_m_<_len_p_holds_
((p_|_n)_^_(p_/^_n))_._m_=_p_._m
let m be Nat; ::_thesis: ( m < len p implies ((p | n) ^ (p /^ n)) . m = p . m )
assume A7: m < len p ; ::_thesis: ((p | n) ^ (p /^ n)) . m = p . m
now__::_thesis:_(_(_m_<_n_&_((p_|_n)_^_(p_/^_n))_._m_=_p_._m_)_or_(_n_<=_m_&_((p_|_n)_^_(p_/^_n))_._m_=_p_._m_)_)
percases ( m < n or n <= m ) ;
case m < n ; ::_thesis: ((p | n) ^ (p /^ n)) . m = p . m
then A8: m in n by NAT_1:44;
hence ((p | n) ^ (p /^ n)) . m = (p | n) . m by A4, AFINSQ_1:def_3
.= p . m by A3, A8, AFINSQ_1:53 ;
::_thesis: verum
end;
case n <= m ; ::_thesis: ((p | n) ^ (p /^ n)) . m = p . m
then max (0,(m - n)) = m - n by FINSEQ_2:4;
then reconsider k = m - n as Element of NAT by FINSEQ_2:5;
k < len (p /^ n) by A5, A7, XREAL_1:9;
then A9: k in dom (p /^ n) by NAT_1:44;
m = (len (p | n)) + k by A4;
hence ((p | n) ^ (p /^ n)) . m = (p /^ n) . k by A9, AFINSQ_1:def_3
.= p . (k + n) by A9, Def2
.= p . m ;
::_thesis: verum
end;
end;
end;
hence ((p | n) ^ (p /^ n)) . m = p . m ; ::_thesis: verum
end;
len ((p | n) ^ (p /^ n)) = n + ((len p) - n) by A5, A4, AFINSQ_1:17
.= len p ;
hence (p | n) ^ (p /^ n) = p by A6, AFINSQ_1:9; ::_thesis: verum
end;
end;
end;
hence (p | n) ^ (p /^ n) = p ; ::_thesis: verum
end;
registration
let D be set ;
let f be XFinSequence of D;
let n be Nat;
clusterf /^ n -> D -valued ;
coherence
f /^ n is D -valued
proof
deffunc H1( Element of NAT ) -> set = f . (D + n);
set p = f /^ n;
percases ( n < len f or len f <= n ) ;
supposeA1: n < len f ; ::_thesis: f /^ n is D -valued
then reconsider k = (len f) - n as Nat by NAT_1:21;
A2: len (f /^ n) = k by A1, Th7;
A3: rng (f /^ n) c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f /^ n) or x in rng f )
assume x in rng (f /^ n) ; ::_thesis: x in rng f
then consider m being Element of NAT such that
A4: m in dom (f /^ n) and
A5: (f /^ n) . m = x by Th3;
m < len (f /^ n) by A4, NAT_1:44;
then m + n < k + n by A2, XREAL_1:6;
then A6: m + n in dom f by NAT_1:44;
(f /^ n) . m = f . (m + n) by A4, Def2;
hence x in rng f by A5, A6, FUNCT_1:def_3; ::_thesis: verum
end;
for f2 being XFinSequence st rng f2 c= D holds
f2 is XFinSequence of D by RELAT_1:def_19;
hence f /^ n is D -valued by A3, XBOOLE_1:1; ::_thesis: verum
end;
suppose len f <= n ; ::_thesis: f /^ n is D -valued
then f /^ n = <%> D by Th6;
hence f /^ n is D -valued ; ::_thesis: verum
end;
end;
end;
end;
definition
let p be XFinSequence;
let k1, k2 be Nat;
func mid (p,k1,k2) -> XFinSequence equals :: AFINSQ_2:def 3
(p | k2) /^ (k1 -' 1);
coherence
(p | k2) /^ (k1 -' 1) is XFinSequence ;
end;
:: deftheorem defines mid AFINSQ_2:def_3_:_
for p being XFinSequence
for k1, k2 being Nat holds mid (p,k1,k2) = (p | k2) /^ (k1 -' 1);
theorem Th14: :: AFINSQ_2:14
for p being XFinSequence
for k1, k2 being Nat st k1 > k2 holds
mid (p,k1,k2) = {}
proof
let p be XFinSequence; ::_thesis: for k1, k2 being Nat st k1 > k2 holds
mid (p,k1,k2) = {}
let k1, k2 be Nat; ::_thesis: ( k1 > k2 implies mid (p,k1,k2) = {} )
set k21 = k2;
A1: len (p | k2) <= k2 by AFINSQ_1:55;
assume A2: k1 > k2 ; ::_thesis: mid (p,k1,k2) = {}
then k1 >= 0 + 1 by NAT_1:13;
then A3: k1 -' 1 = k1 - 1 by XREAL_1:233;
k1 >= k2 + 1 by A2, NAT_1:13;
then k1 - 1 >= (k2 + 1) - 1 by XREAL_1:9;
hence mid (p,k1,k2) = {} by A3, A1, Th6, XXREAL_0:2; ::_thesis: verum
end;
theorem :: AFINSQ_2:15
for p being XFinSequence
for k1, k2 being Nat st 1 <= k1 & k2 <= len p holds
mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
proof
let p be XFinSequence; ::_thesis: for k1, k2 being Nat st 1 <= k1 & k2 <= len p holds
mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
let k1, k2 be Nat; ::_thesis: ( 1 <= k1 & k2 <= len p implies mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) )
assume that
A1: 1 <= k1 and
A2: k2 <= len p ; ::_thesis: mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
set k11 = k1;
set k21 = k2;
A3: len (p | k2) = k2 by A2, AFINSQ_1:54;
k1 < k1 + 1 by NAT_1:13;
then k1 - 1 < (k1 + 1) - 1 by XREAL_1:9;
then A4: k1 -' 1 < k1 by A1, XREAL_1:233;
percases ( k1 <= k2 or k1 > k2 ) ;
supposeA5: k1 <= k2 ; ::_thesis: mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
A6: k2 < k2 + 1 by XREAL_1:29;
then A7: (k2 + 1) -' k1 = (k2 + 1) - k1 by A5, XREAL_1:233, XXREAL_0:2
.= k2 - (k1 - 1) ;
A8: k1 -' 1 = k1 - 1 by A1, XREAL_1:233;
k1 - 1 < k1 by XREAL_1:44;
then k1 - 1 < k2 by A5, XXREAL_0:2;
then A9: len (mid (p,k1,k2)) = k2 - (k1 - 1) by A3, A8, Th7;
then A10: len (mid (p,k1,k2)) = (k2 + 1) - k1 ;
k1 -' 1 < k2 by A4, A5, XXREAL_0:2;
then k1 -' 1 < len p by A2, XXREAL_0:2;
then len (p /^ (k1 -' 1)) = (len p) - (k1 -' 1) by Th7;
then A11: (k2 + 1) -' k1 <= len (p /^ (k1 -' 1)) by A2, A8, A7, XREAL_1:9;
A12: for i being Nat st i < len (mid (p,k1,k2)) holds
(mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i
proof
let i be Nat; ::_thesis: ( i < len (mid (p,k1,k2)) implies (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i )
assume A13: i < len (mid (p,k1,k2)) ; ::_thesis: (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i
then i + (k1 -' 1) < k2 by A8, A9, XREAL_1:20;
then A14: i + (k1 -' 1) in k2 by NAT_1:44;
i + (k1 -' 1) < (k2 - (k1 - 1)) + (k1 -' 1) by A9, A13, XREAL_1:6;
then A15: i + (k1 -' 1) < len p by A2, A8, XXREAL_0:2;
i + (k1 - 1) < k2 by A9, A13, XREAL_1:20;
then A16: ((p | k2) /^ (k1 -' 1)) . i = (p | k2) . (i + (k1 -' 1)) by A3, A8, Th8;
i in (k2 + 1) -' k1 by A7, A9, A13, NAT_1:44;
then ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i = (p /^ (k1 -' 1)) . i by A11, AFINSQ_1:53
.= p . (i + (k1 -' 1)) by A15, Th8 ;
hence (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i by A2, A16, A14, AFINSQ_1:53; ::_thesis: verum
end;
len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) = (k2 + 1) -' k1 by A11, AFINSQ_1:54;
then len (mid (p,k1,k2)) = len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) by A5, A6, A10, XREAL_1:233, XXREAL_0:2;
hence mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) by A12, AFINSQ_1:9; ::_thesis: verum
end;
supposeA17: k1 > k2 ; ::_thesis: mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
then k2 + 1 <= k1 by NAT_1:13;
then A18: (k2 + 1) -' k1 = 0 by NAT_2:8;
mid (p,k1,k2) = {} by A17, Th14;
hence mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) by A18; ::_thesis: verum
end;
end;
end;
theorem Th16: :: AFINSQ_2:16
for k being Nat
for p being XFinSequence holds mid (p,1,k) = p | k
proof
let k be Nat; ::_thesis: for p being XFinSequence holds mid (p,1,k) = p | k
let p be XFinSequence; ::_thesis: mid (p,1,k) = p | k
1 -' 1 = 0 by XREAL_1:232;
hence mid (p,1,k) = p | k by Th10; ::_thesis: verum
end;
theorem :: AFINSQ_2:17
for k being Nat
for p being XFinSequence st len p <= k holds
mid (p,1,k) = p
proof
let k be Nat; ::_thesis: for p being XFinSequence st len p <= k holds
mid (p,1,k) = p
let p be XFinSequence; ::_thesis: ( len p <= k implies mid (p,1,k) = p )
assume A1: len p <= k ; ::_thesis: mid (p,1,k) = p
thus mid (p,1,k) = p | k by Th16
.= p by A1, AFINSQ_1:52 ; ::_thesis: verum
end;
theorem :: AFINSQ_2:18
for k being Nat
for p being XFinSequence holds mid (p,0,k) = mid (p,1,k)
proof
let k be Nat; ::_thesis: for p being XFinSequence holds mid (p,0,k) = mid (p,1,k)
let p be XFinSequence; ::_thesis: mid (p,0,k) = mid (p,1,k)
A1: 0 -' 1 = 0 by NAT_2:8;
mid (p,1,k) = p | k by Th16;
hence mid (p,0,k) = mid (p,1,k) by A1, Th10; ::_thesis: verum
end;
theorem :: AFINSQ_2:19
for p, q being XFinSequence holds mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q
proof
let p, q be XFinSequence; ::_thesis: mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q
A1: ((len p) + 1) -' 1 = len p by NAT_D:34;
len (p ^ q) = (len p) + (len q) by AFINSQ_1:17;
then (p ^ q) | ((len p) + (len q)) = p ^ q by AFINSQ_1:52;
hence mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q by A1, Th12; ::_thesis: verum
end;
registration
let D be set ;
let f be XFinSequence of D;
let k1, k2 be Nat;
cluster mid (f,k1,k2) -> D -valued ;
coherence
mid (f,k1,k2) is D -valued ;
end;
begin
definition
let X be finite natural-membered set ;
func Sgm0 X -> XFinSequence of NAT means :Def4: :: AFINSQ_2:def 4
( rng it = X & ( for l, m, k1, k2 being Nat st l < m & m < len it & k1 = it . l & k2 = it . m holds
k1 < k2 ) );
existence
ex b1 being XFinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
proof
defpred S1[ Nat] means for X being set st X c= $1 holds
ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) );
A1: ex k being Nat st X c= k by Th2;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: for X being set st X c= k holds
ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) ; ::_thesis: S1[k + 1]
let X be set ; ::_thesis: ( X c= k + 1 implies ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A4: X c= k + 1 ; ::_thesis: ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
now__::_thesis:_(_not_X_c=_k_implies_ex_p_being_XFinSequence_of_NAT_st_
(_rng_p_=_X_&_(_for_l,_m,_k1,_k2_being_Nat_st_l_<_m_&_m_<_len_p_&_k1_=_p_._l_&_k2_=_p_._m_holds_
k1_<_k2_)_)_)
set Y = X \ {k};
assume not X c= k ; ::_thesis: ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
then consider x being set such that
A5: x in X and
A6: not x in k by TARSKI:def_3;
reconsider n = x as Element of NAT by A4, A5, Th1;
n < k + 1 by A4, A5, NAT_1:44;
then A7: n <= k by NAT_1:13;
not n < k by A6, NAT_1:44;
then A8: n = k by A7, XXREAL_0:1;
A9: X \ {k} c= k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ {k} or x in k )
assume A10: x in X \ {k} ; ::_thesis: x in k
then A11: x in X ;
then reconsider m = x as Element of NAT by A4, Th1;
not x in {k} by A10, XBOOLE_0:def_5;
then A12: m <> k by TARSKI:def_1;
m < k + 1 by A4, A11, NAT_1:44;
then m <= k by NAT_1:13;
then m < k by A12, XXREAL_0:1;
hence x in k by NAT_1:44; ::_thesis: verum
end;
then consider p being XFinSequence of NAT such that
A13: rng p = X \ {k} and
A14: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 by A3;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
consider q being XFinSequence of NAT such that
A15: q = p ^ <%k%> ;
A16: for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2
proof
let l, m, k1, k2 be Nat; ::_thesis: ( l < m & m < len q & k1 = q . l & k2 = q . m implies k1 < k2 )
assume that
A17: l < m and
A18: m < len q and
A19: k1 = q . l and
A20: k2 = q . m ; ::_thesis: k1 < k2
m + 1 <= len q by A18, NAT_1:13;
then A21: m <= (len q) - 1 by XREAL_1:19;
then l < (len (p ^ <%k%>)) - 1 by A15, A17, XXREAL_0:2;
then l < ((len p) + (len <%k%>)) - 1 by AFINSQ_1:17;
then l < ((len p) + 1) - 1 by AFINSQ_1:34;
then A22: l in dom p by NAT_1:44;
A23: m <= (len q) -' 1 by A21, XREAL_0:def_2;
A24: now__::_thesis:_(_m_<>_(len_q)_-'_1_implies_k1_<_k2_)
A25: k1 = p . l by A15, A19, A22, AFINSQ_1:def_3;
assume m <> (len q) -' 1 ; ::_thesis: k1 < k2
then m < (len (p ^ <%k%>)) -' 1 by A15, A23, XXREAL_0:1;
then m < ((len p) + (len <%k%>)) -' 1 by AFINSQ_1:17;
then m < ((len p) + 1) -' 1 by AFINSQ_1:34;
then A26: m < len p by NAT_D:34;
then m in dom p by NAT_1:44;
then k2 = p . m by A15, A20, AFINSQ_1:def_3;
hence k1 < k2 by A14, A17, A26, A25; ::_thesis: verum
end;
now__::_thesis:_(_m_=_(len_q)_-'_1_implies_k1_<_k2_)
assume m = (len q) -' 1 ; ::_thesis: k1 < k2
then A27: q . m = (p ^ <%k%>) . (((len p) + (len <%k%>)) -' 1) by A15, AFINSQ_1:17
.= (p ^ <%k%>) . (((len p) + 1) -' 1) by AFINSQ_1:34
.= (p ^ <%k%>) . (len p) by NAT_D:34
.= k by AFINSQ_1:36 ;
k1 = p . l by A15, A19, A22, AFINSQ_1:def_3;
then k1 in X \ {k} by A13, A22, FUNCT_1:def_3;
hence k1 < k2 by A9, A20, A27, NAT_1:44; ::_thesis: verum
end;
hence k1 < k2 by A24; ::_thesis: verum
end;
A28: {k} c= X by A5, A8, ZFMISC_1:31;
rng q = (rng p) \/ (rng <%k%>) by A15, AFINSQ_1:26
.= (X \ {k}) \/ {k} by A13, AFINSQ_1:33
.= X \/ {k} by XBOOLE_1:39
.= X by A28, XBOOLE_1:12 ;
hence ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) by A16; ::_thesis: verum
end;
hence ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) by A3; ::_thesis: verum
end;
A29: S1[ 0 ]
proof
let X be set ; ::_thesis: ( X c= 0 implies ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A30: X c= 0 ; ::_thesis: ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
take <%> NAT ; ::_thesis: ( rng (<%> NAT) = X & ( for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds
k1 < k2 ) )
thus rng (<%> NAT) = X by A30; ::_thesis: for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds
k1 < k2
thus for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds
k1 < k2 ; ::_thesis: verum
end;
for k2 being Nat holds S1[k2] from NAT_1:sch_2(A29, A2);
hence ex b1 being XFinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being XFinSequence of NAT st rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
proof
defpred S1[ XFinSequence] means for X being set st ex k being Nat st X c= k & $1 is XFinSequence of NAT & rng $1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len $1 & k1 = $1 . l & k2 = $1 . m holds
k1 < k2 ) holds
for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = $1;
let p, q be XFinSequence of NAT ; ::_thesis: ( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) & rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) implies p = q )
assume that
A31: rng p = X and
A32: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 and
A33: rng q = X and
A34: for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ; ::_thesis: p = q
A35: for p being XFinSequence
for x being set st S1[p] holds
S1[p ^ <%x%>]
proof
let p be XFinSequence; ::_thesis: for x being set st S1[p] holds
S1[p ^ <%x%>]
let x be set ; ::_thesis: ( S1[p] implies S1[p ^ <%x%>] )
assume A36: S1[p] ; ::_thesis: S1[p ^ <%x%>]
let X be set ; ::_thesis: ( ex k being Nat st X c= k & p ^ <%x%> is XFinSequence of NAT & rng (p ^ <%x%>) = X & ( for l, m, k1, k2 being Nat st l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m holds
k1 < k2 ) implies for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = p ^ <%x%> )
given k being Nat such that A37: X c= k ; ::_thesis: ( not p ^ <%x%> is XFinSequence of NAT or not rng (p ^ <%x%>) = X or ex l, m, k1, k2 being Nat st
( l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m & not k1 < k2 ) or for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = p ^ <%x%> )
assume that
A38: p ^ <%x%> is XFinSequence of NAT and
A39: rng (p ^ <%x%>) = X and
A40: for l, m, k1, k2 being Nat st l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m holds
k1 < k2 ; ::_thesis: for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = p ^ <%x%>
let q be XFinSequence of NAT ; ::_thesis: ( rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) implies q = p ^ <%x%> )
assume that
A41: rng q = X and
A42: for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ; ::_thesis: q = p ^ <%x%>
deffunc H1( Nat) -> Element of NAT = q . $1;
len q <> 0
proof
assume len q = 0 ; ::_thesis: contradiction
then p ^ <%x%> = {} by A39, A41, AFINSQ_1:15, RELAT_1:38;
then 0 = len (p ^ <%x%>)
.= (len p) + (len <%x%>) by AFINSQ_1:17
.= 1 + (len p) by AFINSQ_1:34 ;
hence contradiction ; ::_thesis: verum
end;
then consider n being Nat such that
A43: len q = n + 1 by NAT_1:6;
A44: ex m being Nat st
( m = x & ( for l being Nat st l in X & l <> x holds
l < m ) )
proof
<%x%> is XFinSequence of NAT by A38, AFINSQ_1:31;
then rng <%x%> c= NAT by RELAT_1:def_19;
then {x} c= NAT by AFINSQ_1:33;
then reconsider m = x as Element of NAT by ZFMISC_1:31;
take m ; ::_thesis: ( m = x & ( for l being Nat st l in X & l <> x holds
l < m ) )
thus m = x ; ::_thesis: for l being Nat st l in X & l <> x holds
l < m
thus for l being Nat st l in X & l <> x holds
l < m ::_thesis: verum
proof
len <%x%> = 1 by AFINSQ_1:34;
then A45: m = (p ^ <%x%>) . (((len p) + (len <%x%>)) - 1) by AFINSQ_1:36
.= (p ^ <%x%>) . ((len (p ^ <%x%>)) - 1) by AFINSQ_1:17 ;
len (p ^ <%x%>) < (len (p ^ <%x%>)) + 1 by XREAL_1:29;
then A46: (len (p ^ <%x%>)) - 1 < len (p ^ <%x%>) by XREAL_1:19;
let l be Nat; ::_thesis: ( l in X & l <> x implies l < m )
assume that
A47: l in X and
A48: l <> x ; ::_thesis: l < m
consider y being set such that
A49: y in dom (p ^ <%x%>) and
A50: l = (p ^ <%x%>) . y by A39, A47, FUNCT_1:def_3;
reconsider k = y as Element of NAT by A49;
k < len (p ^ <%x%>) by A49, NAT_1:44;
then k < (len p) + (len <%x%>) by AFINSQ_1:17;
then k < (len p) + 1 by AFINSQ_1:34;
then A51: k <= len p by NAT_1:13;
k <> len p by A48, A50, AFINSQ_1:36;
then k < ((len p) + 1) - 1 by A51, XXREAL_0:1;
then k < ((len p) + (len <%x%>)) - 1 by AFINSQ_1:34;
then A52: k < (len (p ^ <%x%>)) - 1 by AFINSQ_1:17;
then (len (p ^ <%x%>)) -' 1 = (len (p ^ <%x%>)) - 1 by XREAL_0:def_2;
hence l < m by A40, A50, A52, A46, A45; ::_thesis: verum
end;
end;
then reconsider m = x as Nat ;
A53: not x in rng p
proof
(len p) + 1 = (len p) + (len <%x%>) by AFINSQ_1:34
.= len (p ^ <%x%>) by AFINSQ_1:17 ;
then A54: len p < len (p ^ <%x%>) by XREAL_1:29;
A55: m = (p ^ <%x%>) . (len p) by AFINSQ_1:36;
assume x in rng p ; ::_thesis: contradiction
then consider y being set such that
A56: y in dom p and
A57: x = p . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A56;
A58: y < len p by A56, NAT_1:44;
m = (p ^ <%x%>) . y by A56, A57, AFINSQ_1:def_3;
hence contradiction by A40, A58, A54, A55; ::_thesis: verum
end;
A59: for z being set holds
( z in ((rng p) \/ {x}) \ {x} iff z in rng p )
proof
let z be set ; ::_thesis: ( z in ((rng p) \/ {x}) \ {x} iff z in rng p )
thus ( z in ((rng p) \/ {x}) \ {x} implies z in rng p ) ::_thesis: ( z in rng p implies z in ((rng p) \/ {x}) \ {x} )
proof
assume A60: z in ((rng p) \/ {x}) \ {x} ; ::_thesis: z in rng p
then not z in {x} by XBOOLE_0:def_5;
hence z in rng p by A60, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A61: z in rng p ; ::_thesis: z in ((rng p) \/ {x}) \ {x}
then A62: z in (rng p) \/ {x} by XBOOLE_0:def_3;
not z in {x} by A53, A61, TARSKI:def_1;
hence z in ((rng p) \/ {x}) \ {x} by A62, XBOOLE_0:def_5; ::_thesis: verum
end;
deffunc H2( set ) -> Element of NAT = q . $1;
consider q9 being XFinSequence such that
A63: len q9 = n and
A64: for m being Nat st m in n holds
q9 . m = H2(m) from AFINSQ_1:sch_2();
now__::_thesis:_for_x_being_set_st_x_in_rng_q9_holds_
x_in_NAT
let x be set ; ::_thesis: ( x in rng q9 implies x in NAT )
assume x in rng q9 ; ::_thesis: x in NAT
then consider y being set such that
A65: y in dom q9 and
A66: x = q9 . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A65;
q . y in NAT ;
hence x in NAT by A63, A64, A65, A66; ::_thesis: verum
end;
then rng q9 c= NAT by TARSKI:def_3;
then reconsider f = q9 as XFinSequence of NAT by RELAT_1:def_19;
A67: p is XFinSequence of NAT by A38, AFINSQ_1:31;
A68: for m being Nat st m in dom <%x%> holds
q . ((len q9) + m) = <%x%> . m
proof
let m be Nat; ::_thesis: ( m in dom <%x%> implies q . ((len q9) + m) = <%x%> . m )
assume m in dom <%x%> ; ::_thesis: q . ((len q9) + m) = <%x%> . m
then m in len <%x%> ;
then A69: m in 1 by AFINSQ_1:34;
0 + 1 = 0 \/ {0} by AFINSQ_1:2;
then A70: m = 0 by A69, TARSKI:def_1;
q . ((len q9) + m) = x
proof
x in {x} by TARSKI:def_1;
then x in rng <%x%> by AFINSQ_1:33;
then x in (rng p) \/ (rng <%x%>) by XBOOLE_0:def_3;
then x in rng q by A39, A41, AFINSQ_1:26;
then consider y being set such that
A71: y in dom q and
A72: x = q . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A71;
y < len q by A71, NAT_1:44;
then y + 1 <= len q by NAT_1:13;
then A73: y <= (len q) - 1 by XREAL_1:19;
len q < (len q) + 1 by XREAL_1:29;
then (len q) - 1 < len q by XREAL_1:19;
then (len q) - 1 in dom q by A43, NAT_1:44;
then A74: q . ((len q) - 1) in X by A41, FUNCT_1:def_3;
len q < (len q) + 1 by XREAL_1:29;
then A75: ( ( y < (len q) - 1 & (len q) - 1 < len q ) or y = (len q) - 1 ) by A73, XREAL_1:19, XXREAL_0:1;
set k = q . ((len q) - 1);
consider d being Nat such that
A76: d = x and
A77: for l being Nat st l in X & l <> x holds
l < d by A44;
assume q . ((len q9) + m) <> x ; ::_thesis: contradiction
then q . ((len q) - 1) < d by A43, A63, A70, A77, A74;
hence contradiction by A42, A43, A76, A72, A75; ::_thesis: verum
end;
hence q . ((len q9) + m) = <%x%> . m by A70, AFINSQ_1:34; ::_thesis: verum
end;
A78: dom q = (len q9) + (len <%x%>) by A43, A63, AFINSQ_1:34;
then A79: q9 ^ <%x%> = q by A63, A64, A68, AFINSQ_1:def_3;
A80: not x in rng f
proof
(len f) + 1 = (len f) + (len <%x%>) by AFINSQ_1:34
.= len (f ^ <%x%>) by AFINSQ_1:17 ;
then A81: len f < len (f ^ <%x%>) by XREAL_1:29;
A82: m = q . (len f) by A79, AFINSQ_1:36;
assume x in rng f ; ::_thesis: contradiction
then consider y being set such that
A83: y in dom f and
A84: x = f . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A83;
A85: y < len f by A83, NAT_1:44;
m = q . y by A63, A64, A83, A84;
hence contradiction by A42, A79, A85, A81, A82; ::_thesis: verum
end;
A86: for z being set holds
( z in ((rng f) \/ {x}) \ {x} iff z in rng f )
proof
let z be set ; ::_thesis: ( z in ((rng f) \/ {x}) \ {x} iff z in rng f )
thus ( z in ((rng f) \/ {x}) \ {x} implies z in rng f ) ::_thesis: ( z in rng f implies z in ((rng f) \/ {x}) \ {x} )
proof
assume A87: z in ((rng f) \/ {x}) \ {x} ; ::_thesis: z in rng f
then not z in {x} by XBOOLE_0:def_5;
hence z in rng f by A87, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A88: z in rng f ; ::_thesis: z in ((rng f) \/ {x}) \ {x}
then A89: z in (rng f) \/ {x} by XBOOLE_0:def_3;
not z in {x} by A80, A88, TARSKI:def_1;
hence z in ((rng f) \/ {x}) \ {x} by A89, XBOOLE_0:def_5; ::_thesis: verum
end;
X = (rng p) \/ (rng <%x%>) by A39, AFINSQ_1:26
.= (rng p) \/ {x} by AFINSQ_1:33 ;
then A90: rng p = X \ {x} by A59, TARSKI:1;
A91: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2
proof
let l, m, k1, k2 be Nat; ::_thesis: ( l < m & m < len p & k1 = p . l & k2 = p . m implies k1 < k2 )
assume that
A92: l < m and
A93: m < len p and
A94: k1 = p . l and
A95: k2 = p . m ; ::_thesis: k1 < k2
l < len p by A92, A93, XXREAL_0:2;
then l in dom p by NAT_1:44;
then A96: k1 = (p ^ <%x%>) . l by A94, AFINSQ_1:def_3;
len p < (len p) + 1 by XREAL_1:29;
then m < (len p) + 1 by A93, XXREAL_0:2;
then m < (len p) + (len <%x%>) by AFINSQ_1:34;
then A97: m < len (p ^ <%x%>) by AFINSQ_1:17;
m in dom p by A93, NAT_1:44;
then k2 = (p ^ <%x%>) . m by A95, AFINSQ_1:def_3;
hence k1 < k2 by A40, A92, A96, A97; ::_thesis: verum
end;
A98: for l, m, k1, k2 being Nat st l < m & m < len f & k1 = f . l & k2 = f . m holds
k1 < k2
proof
let l, m, k1, k2 be Nat; ::_thesis: ( l < m & m < len f & k1 = f . l & k2 = f . m implies k1 < k2 )
assume that
A99: l < m and
A100: m < len f and
A101: k1 = f . l and
A102: k2 = f . m ; ::_thesis: k1 < k2
m in n by A63, A100, NAT_1:44;
then A103: k2 = q . m by A64, A102;
l < n by A63, A99, A100, XXREAL_0:2;
then l in n by NAT_1:44;
then A104: k1 = q . l by A64, A101;
m < len q by A43, A63, A100, NAT_1:13;
hence k1 < k2 by A42, A99, A104, A103; ::_thesis: verum
end;
X = (rng f) \/ (rng <%x%>) by A41, A79, AFINSQ_1:26
.= (rng f) \/ {x} by AFINSQ_1:33 ;
then A105: rng f = X \ {x} by A86, TARSKI:1;
ex m being Nat st X \ {x} c= m by A37, XBOOLE_1:1;
then q9 = p by A36, A91, A67, A90, A98, A105;
hence q = p ^ <%x%> by A63, A64, A78, A68, AFINSQ_1:def_3; ::_thesis: verum
end;
A106: S1[ {} ] ;
A107: for p being XFinSequence holds S1[p] from AFINSQ_1:sch_3(A106, A35);
ex k being Nat st X c= k by Th2;
hence p = q by A31, A32, A33, A34, A107; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Sgm0 AFINSQ_2:def_4_:_
for X being finite natural-membered set
for b2 being XFinSequence of NAT holds
( b2 = Sgm0 X iff ( rng b2 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) ) );
registration
let A be finite natural-membered set ;
cluster Sgm0 A -> one-to-one ;
coherence
Sgm0 A is one-to-one
proof
for x, y being set st x in dom (Sgm0 A) & y in dom (Sgm0 A) & (Sgm0 A) . x = (Sgm0 A) . y holds
not x <> y
proof
let x, y be set ; ::_thesis: ( x in dom (Sgm0 A) & y in dom (Sgm0 A) & (Sgm0 A) . x = (Sgm0 A) . y implies not x <> y )
assume that
A1: x in dom (Sgm0 A) and
A2: y in dom (Sgm0 A) and
A3: (Sgm0 A) . x = (Sgm0 A) . y and
A4: x <> y ; ::_thesis: contradiction
reconsider i = x, j = y as Element of NAT by A1, A2;
percases ( i < j or j < i ) by A4, XXREAL_0:1;
supposeA5: i < j ; ::_thesis: contradiction
j < len (Sgm0 A) by A2, NAT_1:44;
hence contradiction by A3, A5, Def4; ::_thesis: verum
end;
supposeA6: j < i ; ::_thesis: contradiction
i < len (Sgm0 A) by A1, NAT_1:44;
hence contradiction by A3, A6, Def4; ::_thesis: verum
end;
end;
end;
hence Sgm0 A is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
end;
theorem Th20: :: AFINSQ_2:20
for A being finite natural-membered set holds len (Sgm0 A) = card A
proof
let A be finite natural-membered set ; ::_thesis: len (Sgm0 A) = card A
rng (Sgm0 A) = A by Def4;
then len (Sgm0 A),A are_equipotent by WELLORD2:def_4;
then card A = card (len (Sgm0 A)) by CARD_1:5;
hence len (Sgm0 A) = card A ; ::_thesis: verum
end;
theorem Th21: :: AFINSQ_2:21
for X, Y being finite natural-membered set st X c= Y & X <> {} holds
(Sgm0 Y) . 0 <= (Sgm0 X) . 0
proof
let X, Y be finite natural-membered set ; ::_thesis: ( X c= Y & X <> {} implies (Sgm0 Y) . 0 <= (Sgm0 X) . 0 )
assume that
A1: X c= Y and
A2: X <> {} ; ::_thesis: (Sgm0 Y) . 0 <= (Sgm0 X) . 0
reconsider X0 = X as finite set ;
0 <> card X0 by A2;
then 0 < len (Sgm0 X) by Th20;
then A3: 0 in dom (Sgm0 X) by NAT_1:44;
A4: rng (Sgm0 Y) = Y by Def4;
rng (Sgm0 X) = X by Def4;
then (Sgm0 X) . 0 in X by A3, FUNCT_1:def_3;
then consider x being set such that
A5: x in dom (Sgm0 Y) and
A6: (Sgm0 Y) . x = (Sgm0 X) . 0 by A1, A4, FUNCT_1:def_3;
reconsider nx = x as Nat by A5;
A7: nx < len (Sgm0 Y) by A5, NAT_1:44;
now__::_thesis:_(_(_0_<>_nx_&_(Sgm0_Y)_._0_<=_(Sgm0_X)_._0_)_or_(_0_=_nx_&_(Sgm0_Y)_._0_<=_(Sgm0_X)_._0_)_)
percases ( 0 <> nx or 0 = nx ) ;
case 0 <> nx ; ::_thesis: (Sgm0 Y) . 0 <= (Sgm0 X) . 0
hence (Sgm0 Y) . 0 <= (Sgm0 X) . 0 by A6, A7, Def4; ::_thesis: verum
end;
case 0 = nx ; ::_thesis: (Sgm0 Y) . 0 <= (Sgm0 X) . 0
hence (Sgm0 Y) . 0 <= (Sgm0 X) . 0 by A6; ::_thesis: verum
end;
end;
end;
hence (Sgm0 Y) . 0 <= (Sgm0 X) . 0 ; ::_thesis: verum
end;
theorem Th22: :: AFINSQ_2:22
for n being Nat holds (Sgm0 {n}) . 0 = n
proof
let n be Nat; ::_thesis: (Sgm0 {n}) . 0 = n
len (Sgm0 {n}) = card {n} by Th20;
then 0 in dom (Sgm0 {n}) by NAT_1:44;
then A1: (Sgm0 {n}) . 0 in rng (Sgm0 {n}) by FUNCT_1:def_3;
rng (Sgm0 {n}) = {n} by Def4;
hence (Sgm0 {n}) . 0 = n by A1, TARSKI:def_1; ::_thesis: verum
end;
definition
let B1, B2 be set ;
predB1 _{}
set x = the Element of (B1 /\ B2) /\ NAT;
reconsider nx = the Element of (B1 /\ B2) /\ NAT as Nat ;
assume (B1 /\ B2) /\ NAT <> {} ; ::_thesis: contradiction
then A2: the Element of (B1 /\ B2) /\ NAT in B1 /\ B2 by XBOOLE_0:def_4;
then A3: nx in B2 by XBOOLE_0:def_4;
nx in B1 by A2, XBOOLE_0:def_4;
hence contradiction by A1, A3, Def5; ::_thesis: verum
end;
hence (B1 /\ B2) /\ NAT = {} ; ::_thesis: verum
end;
theorem :: AFINSQ_2:24
for B1, B2 being finite natural-membered set st B1 {} by XBOOLE_0:def_7;
then A3: the Element of B1 /\ B2 in B2 by XBOOLE_0:def_4;
the Element of B1 /\ B2 in B1 by A2, XBOOLE_0:def_4;
hence contradiction by A1, A3, Def5; ::_thesis: verum
end;
hence B1 misses B2 ; ::_thesis: verum
end;
theorem Th25: :: AFINSQ_2:25
for A, B1, B2 being set st B1 {} & ex x being set st
( x in X & {x} {} & ex x being set st
( x in X & {x} {} and
A2: ex x being set st
( x in X & {x} card Y by A1;
then 0 < len (Sgm0 Y) by Th20;
then A5: 0 in dom (Sgm0 Y) by NAT_1:44;
rng (Sgm0 Y) = Y by Def4;
then A6: (Sgm0 Y) . 0 in Y by A5, FUNCT_1:def_3;
reconsider x0 = x as Element of NAT by A3, ORDINAL1:def_12;
set nx = x0;
x0 in {x0} by TARSKI:def_1;
then A7: x0 <= (Sgm0 Y) . 0 by A4, A6, Def6;
{x0} c= X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x0} or y in X )
assume y in {x0} ; ::_thesis: y in X
hence y in X by A3, TARSKI:def_1; ::_thesis: verum
end;
then A8: (Sgm0 X) . 0 <= (Sgm0 {x0}) . 0 by Th21;
(Sgm0 {x0}) . 0 = x0 by Th22;
hence (Sgm0 X) . 0 <= (Sgm0 Y) . 0 by A8, A7, XXREAL_0:2; ::_thesis: verum
end;
theorem Th27: :: AFINSQ_2:27
for i being Nat
for X0, Y0 being finite natural-membered set st X0 {} by A2, CARD_1:27, XBOOLE_1:15;
A18: now__::_thesis:_(_not__{__v_where_v_is_Element_of_X0_\/_Y0_:_ex_k2_being_Nat_st_
(_v_=_((Sgm0_(X0_\/_Y0))_|_(card_X0))_._k2_&_k2_in_card_X0_)__}__c=_X0_implies_X0_c=__{__v_where_v_is_Element_of_X0_\/_Y0_:_ex_k2_being_Nat_st_
(_v_=_((Sgm0_(X0_\/_Y0))_|_(card_X0))_._k2_&_k2_in_card_X0_)__}__)
assume that
A19: not { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } c= X0 and
A20: not X0 c= { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } ; ::_thesis: contradiction
consider v1 being set such that
A21: v1 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } and
A22: not v1 in X0 by A19, TARSKI:def_3;
consider v10 being Element of X0 \/ Y0 such that
A23: v1 = v10 and
A24: ex k2 being Nat st
( v10 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) by A21;
A25: v10 in Y0 by A17, A22, A23, XBOOLE_0:def_3;
reconsider nv10 = v10 as Nat ;
consider v2 being set such that
A26: v2 in X0 and
A27: not v2 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } by A20, TARSKI:def_3;
X0 c= X0 \/ Y0 by XBOOLE_1:7;
then consider x2 being set such that
A28: x2 in dom (Sgm0 (X0 \/ Y0)) and
A29: v2 = (Sgm0 (X0 \/ Y0)) . x2 by A11, A26, FUNCT_1:def_3;
reconsider x20 = x2 as Nat by A28;
reconsider nv2 = v2 as Nat by A29;
A30: x20 < len (Sgm0 (X0 \/ Y0)) by A28, NAT_1:44;
A31: now__::_thesis:_not_x20_<_card_X0
assume x20 < card X0 ; ::_thesis: contradiction
then A32: x20 in card X0 by NAT_1:44;
card X0 <= card (X0 \/ Y0) by NAT_1:43, XBOOLE_1:7;
then card X0 <= len (Sgm0 (X0 \/ Y0)) by Th20;
then ((Sgm0 (X0 \/ Y0)) | (card X0)) . x20 = (Sgm0 (X0 \/ Y0)) . x20 by A32, AFINSQ_1:53;
hence contradiction by A4, A26, A27, A29, A32; ::_thesis: verum
end;
consider k20 being Nat such that
A33: v10 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k20 and
A34: k20 in card X0 by A24;
card X0 <= len (Sgm0 (X0 \/ Y0)) by A10, NAT_1:43, XBOOLE_1:7;
then A35: ((Sgm0 (X0 \/ Y0)) | (card X0)) . k20 = (Sgm0 (X0 \/ Y0)) . k20 by A34, AFINSQ_1:53;
k20 < len ((Sgm0 (X0 \/ Y0)) | (card X0)) by A6, A34, NAT_1:44;
then k20 < x20 by A6, A31, XXREAL_0:2;
then nv10 < nv2 by A33, A29, A35, A30, Def4;
hence contradiction by A1, A26, A25, Def5; ::_thesis: verum
end;
A36: now__::_thesis:_(_(_Z0_c=_X0_&_Z0_=_X0_)_or_(_X0_c=_Z0_&_Z0_=_X0_)_)
percases ( Z0 c= X0 or X0 c= Z0 ) by A18;
case Z0 c= X0 ; ::_thesis: Z0 = X0
hence Z0 = X0 by A16, Lm1; ::_thesis: verum
end;
case X0 c= Z0 ; ::_thesis: Z0 = X0
hence Z0 = X0 by A16, Lm1; ::_thesis: verum
end;
end;
end;
card X0 <= len (Sgm0 (X0 \/ Y0)) by A5, NAT_1:43, XBOOLE_1:7;
hence ( rng ((Sgm0 (X0 \/ Y0)) | (card X0)) = X0 & ((Sgm0 (X0 \/ Y0)) | (card X0)) . i = (Sgm0 (X0 \/ Y0)) . i ) by A12, A7, A36, A3, AFINSQ_1:53, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: AFINSQ_2:28
for i being Nat
for X, Y being finite natural-membered set st X {} by A2, CARD_1:27, XBOOLE_1:15;
A12: now__::_thesis:_(_not__{__v_where_v_is_Element_of_X_\/_Y_:_ex_k2_being_Nat_st_
(_v_=_((Sgm0_(X_\/_Y))_|_(card_X))_._k2_&_k2_in_card_X_)__}__c=_X_implies_X_c=__{__v_where_v_is_Element_of_X_\/_Y_:_ex_k2_being_Nat_st_
(_v_=_((Sgm0_(X_\/_Y))_|_(card_X))_._k2_&_k2_in_card_X_)__}__)
assume that
A13: not { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } c= X and
A14: not X c= { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ; ::_thesis: contradiction
consider v1 being set such that
A15: v1 in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } and
A16: not v1 in X by A13, TARSKI:def_3;
consider v10 being Element of X \/ Y such that
A17: v1 = v10 and
A18: ex k2 being Nat st
( v10 = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) by A15;
A19: v10 in Y by A11, A16, A17, XBOOLE_0:def_3;
reconsider nv10 = v10 as Nat ;
consider v2 being set such that
A20: v2 in X and
A21: not v2 in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } by A14, TARSKI:def_3;
X c= X \/ Y by XBOOLE_1:7;
then consider x2 being set such that
A22: x2 in dom (Sgm0 (X \/ Y)) and
A23: v2 = (Sgm0 (X \/ Y)) . x2 by A3, A20, FUNCT_1:def_3;
reconsider x20 = x2 as Nat by A22;
now__::_thesis:_not_x20_<_card_X
assume x20 < card X ; ::_thesis: contradiction
then A24: x20 in card X by NAT_1:44;
card X <= card (X \/ Y) by NAT_1:43, XBOOLE_1:7;
then card X <= len (Sgm0 (X \/ Y)) by Th20;
then ((Sgm0 (X \/ Y)) | (card X)) . x20 = (Sgm0 (X \/ Y)) . x20 by A24, AFINSQ_1:53;
hence contradiction by A5, A10, A21, A23, A24, FUNCT_1:def_3; ::_thesis: verum
end;
then A25: len ((Sgm0 (X \/ Y)) | (card X)) <= x20 by A4, AFINSQ_1:54;
consider k20 being Nat such that
A26: v10 = ((Sgm0 (X \/ Y)) | (card X)) . k20 and
A27: k20 in card X by A18;
A28: ((Sgm0 (X \/ Y)) | (card X)) . k20 = (Sgm0 (X \/ Y)) . k20 by A4, A27, AFINSQ_1:53;
reconsider nv2 = v2 as Nat by A23;
k20 < len ((Sgm0 (X \/ Y)) | (card X)) by A5, A27, NAT_1:44;
then A29: k20 < x20 by A25, XXREAL_0:2;
x20 < len (Sgm0 (X \/ Y)) by A22, NAT_1:44;
then nv10 < nv2 by A26, A23, A29, A28, Def4;
hence contradiction by A1, A20, A19, Def5; ::_thesis: verum
end;
(Sgm0 (X \/ Y)) | (card X) is one-to-one by FUNCT_1:52;
then A30: dom ((Sgm0 (X \/ Y)) | (card X)),((Sgm0 (X \/ Y)) | (card X)) .: (dom ((Sgm0 (X \/ Y)) | (card X))) are_equipotent by CARD_1:33;
((Sgm0 (X \/ Y)) | (card X)) .: (dom ((Sgm0 (X \/ Y)) | (card X))) = rng ((Sgm0 (X \/ Y)) | (card X)) by RELAT_1:113;
then A31: card { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } = card (len ((Sgm0 (X \/ Y)) | (card X))) by A10, A30, CARD_1:5;
then A32: card { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } = card X by A4, AFINSQ_1:54;
A33: now__::_thesis:_(_(_Z0_c=_X_&_Z0_=_X_)_or_(_X_c=_Z0_&_Z0_=_X_)_)
percases ( Z0 c= X or X c= Z0 ) by A12;
case Z0 c= X ; ::_thesis: Z0 = X
hence Z0 = X by A4, A31, Lm1, AFINSQ_1:54; ::_thesis: verum
end;
case X c= Z0 ; ::_thesis: Z0 = X
hence Z0 = X by A32, Lm1; ::_thesis: verum
end;
end;
end;
((Sgm0 (X \/ Y)) | (card X)) . i = (Sgm0 (X \/ Y)) . i by A2, A4, AFINSQ_1:53;
hence (Sgm0 (X \/ Y)) . i in X by A2, A5, A10, A33, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th29: :: AFINSQ_2:29
for i being Nat
for X, Y being finite natural-membered set st X {} by A2, CARD_1:27, XBOOLE_1:15;
A22: now__::_thesis:_(_not__{__v_where_v_is_Element_of_X0_\/_Y0_:_ex_k2_being_Nat_st_
(_v_=_((Sgm0_(X0_\/_Y0))_/^_(card_X0))_._k2_&_k2_in_card_Y0_)__}__c=_Y0_implies_Y0_c=__{__v_where_v_is_Element_of_X0_\/_Y0_:_ex_k2_being_Nat_st_
(_v_=_((Sgm0_(X0_\/_Y0))_/^_(card_X0))_._k2_&_k2_in_card_Y0_)__}__)
assume that
A23: not { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } c= Y0 and
A24: not Y0 c= { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } ; ::_thesis: contradiction
consider v2 being set such that
A25: v2 in Y0 and
A26: not v2 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } by A24, TARSKI:def_3;
Y0 c= X0 \/ Y0 by XBOOLE_1:7;
then consider x2 being set such that
A27: x2 in dom (Sgm0 (X0 \/ Y0)) and
A28: v2 = (Sgm0 (X0 \/ Y0)) . x2 by A6, A25, FUNCT_1:def_3;
consider v1 being set such that
A29: v1 in { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } and
A30: not v1 in Y0 by A23, TARSKI:def_3;
consider v10 being Element of X0 \/ Y0 such that
A31: v1 = v10 and
A32: ex k2 being Nat st
( v10 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) by A29;
A33: v10 in X0 by A21, A30, A31, XBOOLE_0:def_3;
reconsider nv10 = v10 as Nat ;
reconsider nv2 = v2 as Nat by A28;
consider k20 being Nat such that
A34: v10 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k20 and
A35: k20 in card Y0 by A32;
k20 < card Y0 by A35, NAT_1:44;
then A36: k20 + (card X0) < len (Sgm0 (X0 \/ Y0)) by A20, XREAL_1:6;
then A37: ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k20 = (Sgm0 (X0 \/ Y0)) . (k20 + (card X0)) by Th8;
reconsider x20 = x2 as Nat by A27;
set nx20 = x20 -' (card X0);
A38: v2 in X0 \/ Y0 by A6, A27, A28, FUNCT_1:def_3;
A39: now__::_thesis:_not_x20_>=_card_X0
assume A40: x20 >= card X0 ; ::_thesis: contradiction
then A41: x20 -' (card X0) = x20 - (card X0) by XREAL_1:233;
x20 < (card X0) + (card Y0) by A20, A27, NAT_1:44;
then x20 - (card X0) < ((card X0) + (card Y0)) - (card X0) by XREAL_1:9;
then A42: x20 -' (card X0) < card Y0 by A40, XREAL_1:233;
then A43: x20 -' (card X0) in card Y0 by NAT_1:44;
(x20 -' (card X0)) + (card X0) < len (Sgm0 (X0 \/ Y0)) by A20, A42, XREAL_1:6;
then ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . (x20 -' (card X0)) = (Sgm0 (X0 \/ Y0)) . x20 by A41, Th8;
hence contradiction by A26, A28, A38, A43; ::_thesis: verum
end;
card X0 <= (card X0) + k20 by NAT_1:12;
then k20 + (card X0) > x20 by A39, XXREAL_0:2;
then nv10 > nv2 by A34, A28, A36, A37, Def4;
hence contradiction by A1, A25, A33, Def5; ::_thesis: verum
end;
A44: now__::_thesis:_(_(_Z0_c=_Y0_&_Z0_=_Y0_)_or_(_Y0_c=_Z0_&_Z0_=_Y0_)_)
percases ( Z0 c= Y0 or Y0 c= Z0 ) by A22;
case Z0 c= Y0 ; ::_thesis: Z0 = Y0
hence Z0 = Y0 by A19, Lm1; ::_thesis: verum
end;
case Y0 c= Z0 ; ::_thesis: Z0 = Y0
hence Z0 = Y0 by A19, Lm1; ::_thesis: verum
end;
end;
end;
i + (card X0) < len (Sgm0 (X0 \/ Y0)) by A2, A9, A11, XREAL_1:20;
hence ( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) ) by A15, A12, A44, Th8, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th31: :: AFINSQ_2:31
for i being Nat
for X, Y being finite natural-membered set st X {} & X {} & X {} and
A2: X 0 by A1;
then 0 < len (Sgm0 Y) by Th20;
then (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (0 + (len (Sgm0 X))) by A2, Th31;
hence (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X)) ; ::_thesis: verum
end;
theorem Th33: :: AFINSQ_2:33
for l, m, n, k being Nat
for X being finite natural-membered set st k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l holds
m < n
proof
let l, m, n, k be Nat; ::_thesis: for X being finite natural-membered set st k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l holds
m < n
let X be finite natural-membered set ; ::_thesis: ( k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l implies m < n )
assume that
A1: k < l and
A2: m < len (Sgm0 X) and
A3: (Sgm0 X) . m = k and
A4: (Sgm0 X) . n = l and
A5: not m < n ; ::_thesis: contradiction
n < m by A1, A3, A4, A5, XXREAL_0:1;
hence contradiction by A1, A2, A3, A4, Def4; ::_thesis: verum
end;
theorem Th34: :: AFINSQ_2:34
for X, Y being finite natural-membered set st X <> {} & X {} & X {} and
A2: X 0 by A1;
then 0 < len (Sgm0 X) by Th20;
hence (Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0 by A2, Th29; ::_thesis: verum
end;
theorem Th35: :: AFINSQ_2:35
for X, Y being finite natural-membered set holds
( X (Sgm0 X) . (k + 1) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( k in dom (Sgm0 X) or not k in dom (Sgm0 X) ) ;
supposeA14: k in dom (Sgm0 X) ; ::_thesis: contradiction
set m1 = (Sgm0 (X \/ Y)) . k;
set n1 = (Sgm0 X) . k;
now__::_thesis:_contradiction
percases ( (Sgm0 (X \/ Y)) . (k + 1) < (Sgm0 X) . (k + 1) or (Sgm0 X) . (k + 1) < (Sgm0 (X \/ Y)) . (k + 1) ) by A13, XXREAL_0:1;
supposeA15: (Sgm0 (X \/ Y)) . (k + 1) < (Sgm0 X) . (k + 1) ; ::_thesis: contradiction
then not (Sgm0 (X \/ Y)) . (k + 1) in Y by A1, A10, Def5;
then (Sgm0 (X \/ Y)) . (k + 1) in X by A12, XBOOLE_0:def_3;
then (Sgm0 (X \/ Y)) . (k + 1) in rng (Sgm0 X) by Def4;
then consider x being set such that
A16: x in dom (Sgm0 X) and
A17: (Sgm0 X) . x = (Sgm0 (X \/ Y)) . (k + 1) by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A16;
x < len (Sgm0 X) by A16, NAT_1:44;
then A18: x < k + 1 by A15, A17, Th33;
A19: k < k + 1 by XREAL_1:29;
k + 1 < len (Sgm0 (X \/ Y)) by A9, A11, NAT_1:44;
then A20: (Sgm0 X) . k < (Sgm0 (X \/ Y)) . (k + 1) by A8, A14, A19, Def4;
k < len (Sgm0 X) by A14, NAT_1:44;
then k < x by A17, A20, Th33;
hence contradiction by A18, NAT_1:13; ::_thesis: verum
end;
supposeA21: (Sgm0 X) . (k + 1) < (Sgm0 (X \/ Y)) . (k + 1) ; ::_thesis: contradiction
(Sgm0 X) . (k + 1) in X \/ Y by A10, XBOOLE_0:def_3;
then (Sgm0 X) . (k + 1) in rng (Sgm0 (X \/ Y)) by Def4;
then consider x being set such that
A22: x in dom (Sgm0 (X \/ Y)) and
A23: (Sgm0 (X \/ Y)) . x = (Sgm0 X) . (k + 1) by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A22;
x < len (Sgm0 (X \/ Y)) by A22, NAT_1:44;
then A24: x < k + 1 by A21, A23, Th33;
A25: k < k + 1 by XREAL_1:29;
k + 1 < len (Sgm0 X) by A9, NAT_1:44;
then A26: (Sgm0 (X \/ Y)) . k < (Sgm0 X) . (k + 1) by A8, A14, A25, Def4;
k < len (Sgm0 (X \/ Y)) by A11, A14, NAT_1:44;
then k < x by A23, A26, Th33;
hence contradiction by A24, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
supposeA27: not k in dom (Sgm0 X) ; ::_thesis: contradiction
A28: k < k + 1 by XREAL_1:29;
len (Sgm0 X) <= k by A27, NAT_1:44;
then len (Sgm0 X) < k + 1 by A28, XXREAL_0:2;
hence contradiction by A9, NAT_1:44; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
( 0 < len (Sgm0 X) implies X1 <> {} ) by Th20, CARD_1:27;
then A29: S1[ 0 ] by A1, Th34;
A30: for k being Nat holds S1[k] from NAT_1:sch_2(A29, A7);
defpred S2[ Nat] means ( $1 in dom (Sgm0 Y) implies (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + $1) = (Sgm0 Y) . $1 );
A31: now__::_thesis:_for_k_being_Nat_st_S2[k]_holds_
S2[k_+_1]
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A32: S2[k] ; ::_thesis: S2[k + 1]
thus S2[k + 1] ::_thesis: verum
proof
set n = (Sgm0 Y) . (k + 1);
set a = (len (Sgm0 X)) + (k + 1);
set m = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1));
assume A33: k + 1 in dom (Sgm0 Y) ; ::_thesis: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) = (Sgm0 Y) . (k + 1)
then (Sgm0 Y) . (k + 1) in rng (Sgm0 Y) by FUNCT_1:def_3;
then A34: (Sgm0 Y) . (k + 1) in Y by Def4;
k + 1 < len (Sgm0 Y) by A33, NAT_1:44;
then A35: (len (Sgm0 X)) + (k + 1) < len (Sgm0 (X \/ Y)) by A6, XREAL_1:6;
then A36: (len (Sgm0 X)) + (k + 1) in dom (Sgm0 (X \/ Y)) by NAT_1:44;
then (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 (X \/ Y)) by FUNCT_1:def_3;
then A37: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in X \/ Y by Def4;
A38: now__::_thesis:_not_(Sgm0_(X_\/_Y))_._((len_(Sgm0_X))_+_(k_+_1))_in_X
A39: len (Sgm0 X) <= len (Sgm0 (X \/ Y)) by A6, NAT_1:12;
assume (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in X ; ::_thesis: contradiction
then (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 X) by Def4;
then consider x being set such that
A40: x in dom (Sgm0 X) and
A41: (Sgm0 X) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A40;
x < len (Sgm0 X) by A40, NAT_1:44;
then x < len (Sgm0 (X \/ Y)) by A39, XXREAL_0:2;
then A42: x in dom (Sgm0 (X \/ Y)) by NAT_1:44;
(Sgm0 (X \/ Y)) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by A30, A40, A41;
then x = (len (Sgm0 X)) + (k + 1) by A36, A42, FUNCT_1:def_4;
then (len (Sgm0 X)) + (k + 1) <= (len (Sgm0 X)) + 0 by A40, NAT_1:44;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
assume A43: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) <> (Sgm0 Y) . (k + 1) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( k in dom (Sgm0 Y) or not k in dom (Sgm0 Y) ) ;
supposeA44: k in dom (Sgm0 Y) ; ::_thesis: contradiction
set m1 = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + k);
set n1 = (Sgm0 Y) . k;
A45: k < len (Sgm0 Y) by A44, NAT_1:44;
now__::_thesis:_contradiction
percases ( (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) < (Sgm0 Y) . (k + 1) or (Sgm0 Y) . (k + 1) < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) ) by A43, XXREAL_0:1;
supposeA46: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) < (Sgm0 Y) . (k + 1) ; ::_thesis: contradiction
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in Y by A37, A38, XBOOLE_0:def_3;
then (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 Y) by Def4;
then consider x being set such that
A47: x in dom (Sgm0 Y) and
A48: (Sgm0 Y) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A47;
x < len (Sgm0 Y) by A47, NAT_1:44;
then A49: x < k + 1 by A46, A48, Th33;
(len (Sgm0 X)) + k < ((len (Sgm0 X)) + k) + 1 by XREAL_1:29;
then A50: (Sgm0 Y) . k < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) by A32, A35, A44, Def4;
k < len (Sgm0 Y) by A44, NAT_1:44;
then k < x by A48, A50, Th33;
hence contradiction by A49, NAT_1:13; ::_thesis: verum
end;
supposeA51: (Sgm0 Y) . (k + 1) < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) ; ::_thesis: contradiction
(Sgm0 Y) . (k + 1) in X \/ Y by A34, XBOOLE_0:def_3;
then (Sgm0 Y) . (k + 1) in rng (Sgm0 (X \/ Y)) by Def4;
then consider x being set such that
A52: x in dom (Sgm0 (X \/ Y)) and
A53: (Sgm0 (X \/ Y)) . x = (Sgm0 Y) . (k + 1) by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A52;
x < len (Sgm0 (X \/ Y)) by A52, NAT_1:44;
then A54: x < ((len (Sgm0 X)) + k) + 1 by A51, A53, Th33;
A55: k < k + 1 by XREAL_1:29;
k + 1 < len (Sgm0 Y) by A33, NAT_1:44;
then A56: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + k) < (Sgm0 Y) . (k + 1) by A32, A44, A55, Def4;
(len (Sgm0 X)) + k < len (Sgm0 (X \/ Y)) by A6, A45, XREAL_1:6;
then (len (Sgm0 X)) + k < x by A53, A56, Th33;
hence contradiction by A54, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
supposeA57: not k in dom (Sgm0 Y) ; ::_thesis: contradiction
A58: k < k + 1 by XREAL_1:29;
len (Sgm0 Y) <= k by A57, NAT_1:44;
then len (Sgm0 Y) < k + 1 by A58, XXREAL_0:2;
hence contradiction by A33, NAT_1:44; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
( len (Sgm0 Y) > 0 implies Y <> {} ) by Th20, CARD_1:27;
then A59: S2[ 0 ] by A1, Th32;
for k being Nat holds S2[k] from NAT_1:sch_2(A59, A31);
hence Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) by A6, A30, AFINSQ_1:def_3; ::_thesis: verum
end;
assume A60: Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) ; ::_thesis: X XFinSequence equals :: AFINSQ_2:def 7
f * (Sgm0 (B /\ (len f)));
coherence
f * (Sgm0 (B /\ (len f))) is XFinSequence
proof
B /\ (len f) c= dom f by XBOOLE_1:17;
then rng (Sgm0 (B /\ (len f))) c= dom f by Def4;
hence f * (Sgm0 (B /\ (len f))) is XFinSequence by AFINSQ_1:10; ::_thesis: verum
end;
end;
:: deftheorem defines SubXFinS AFINSQ_2:def_7_:_
for f being XFinSequence
for B being set holds SubXFinS (f,B) = f * (Sgm0 (B /\ (len f)));
theorem Th36: :: AFINSQ_2:36
for p being XFinSequence
for B being set holds
( len (SubXFinS (p,B)) = card (B /\ (len p)) & ( for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) ) )
proof
let p be XFinSequence; ::_thesis: for B being set holds
( len (SubXFinS (p,B)) = card (B /\ (len p)) & ( for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) ) )
let B be set ; ::_thesis: ( len (SubXFinS (p,B)) = card (B /\ (len p)) & ( for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) ) )
B /\ (len p) c= dom p by XBOOLE_1:17;
then rng (Sgm0 (B /\ (len p))) c= dom p by Def4;
then dom (SubXFinS (p,B)) = len (Sgm0 (B /\ (len p))) by RELAT_1:27
.= card (B /\ (len p)) by Th20 ;
hence len (SubXFinS (p,B)) = card (B /\ (len p)) ; ::_thesis: for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i)
let i be Nat; ::_thesis: ( i < len (SubXFinS (p,B)) implies (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) )
assume i < len (SubXFinS (p,B)) ; ::_thesis: (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i)
then i in dom (SubXFinS (p,B)) by NAT_1:44;
hence (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) by FUNCT_1:12; ::_thesis: verum
end;
registration
let D be set ;
let f be XFinSequence of D;
let B be set ;
cluster SubXFinS (f,B) -> D -valued ;
coherence
SubXFinS (f,B) is D -valued ;
end;
registration
let p be XFinSequence;
cluster SubXFinS (p,{}) -> empty ;
coherence
SubXFinS (p,{}) is empty
proof
len (SubXFinS (p,{})) = card {} by Th36;
hence SubXFinS (p,{}) is empty ; ::_thesis: verum
end;
end;
registration
let B be set ;
cluster SubXFinS ({},B) -> empty ;
coherence
SubXFinS ({},B) is empty ;
end;
registration
let n be Nat;
let x be set ;
clustern --> x -> T-Sequence-like ;
coherence
n --> x is T-Sequence-like ;
end;
scheme :: AFINSQ_2:sch 2
Sch5{ F1() -> set , P1[ set ] } :
for F being XFinSequence of F1() holds P1[F]
provided
A1: P1[ <%> F1()] and
A2: for F being XFinSequence of F1()
for d being Element of F1() st P1[F] holds
P1[F ^ <%d%>]
proof
defpred S1[ set ] means for F being XFinSequence of F1() st len F = $1 holds
P1[F];
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: for F being XFinSequence of F1() st len F = n holds
P1[F] ; ::_thesis: S1[n + 1]
let F be XFinSequence of F1(); ::_thesis: ( len F = n + 1 implies P1[F] )
assume A5: len F = n + 1 ; ::_thesis: P1[F]
then F <> {} ;
then consider G being XFinSequence, d being set such that
A6: F = G ^ <%d%> by AFINSQ_1:40;
reconsider G = G, dd = <%d%> as XFinSequence of F1() by A6, AFINSQ_1:31;
A7: ( rng dd c= F1() & rng dd = {d} & d in {d} ) by AFINSQ_1:33, TARSKI:def_1;
len dd = 1 by AFINSQ_1:34;
then len F = (len G) + 1 by A6, AFINSQ_1:17;
hence P1[F] by A2, A4, A5, A6, A7; ::_thesis: verum
end;
let F be XFinSequence of F1(); ::_thesis: P1[F]
A8: len F = len F ;
for X being set st card X = {} holds
X = {} ;
then A9: S1[ 0 ] by A1;
for n being Nat holds S1[n] from NAT_1:sch_2(A9, A3);
hence P1[F] by A8; ::_thesis: verum
end;
definition
let D be non empty set ;
let F be XFinSequence;
assume A1: F is D -valued ;
let b be BinOp of D;
assume A2: ( b is having_a_unity or len F >= 1 ) ;
funcb "**" F -> Element of D means :Def8: :: AFINSQ_2:def 8
it = the_unity_wrt b if ( b is having_a_unity & len F = 0 )
otherwise ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & it = f . ((len F) - 1) );
existence
( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) )
proof
now__::_thesis:_(_(_b_is_having_a_unity_&_len_F_=_0_implies_ex_b1_being_Element_of_D_st_b1_=_the_unity_wrt_b_)_&_(_(_not_b_is_having_a_unity_or_not_len_F_=_0_)_implies_ex_b1_being_Element_of_D_ex_f_being_Function_of_NAT,D_st_
(_f_._0_=_F_._0_&_(_for_n_being_Nat_st_n_+_1_<_len_F_holds_
f_._(n_+_1)_=_b_._((f_._n),(F_._(n_+_1)))_)_&_b1_=_f_._((len_F)_-_1)_)_)_)
percases ( len F = 0 or len F <> 0 ) ;
suppose len F = 0 ; ::_thesis: ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) )
hence ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) ) by A2; ::_thesis: verum
end;
supposeA3: len F <> 0 ; ::_thesis: ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) )
defpred S1[ Nat] means for F being XFinSequence of D st len F = $1 & len F <> 0 holds
ex d being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) );
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; ::_thesis: S1[k + 1]
let F be XFinSequence of D; ::_thesis: ( len F = k + 1 & len F <> 0 implies ex d being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) )
assume that
A6: len F = k + 1 and
len F <> 0 ; ::_thesis: ex d being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) )
set G = F | k;
A7: k < k + 1 by NAT_1:13;
then A8: len (F | k) = k by A6, AFINSQ_1:11;
now__::_thesis:_ex_d_being_Element_of_D_ex_f_being_Function_of_NAT,D_st_
(_f_._0_=_F_._0_&_(_for_n_being_Nat_st_n_+_1_<_len_F_holds_
f_._(n_+_1)_=_b_._((f_._n),(F_._(n_+_1)))_)_&_d_=_f_._((len_F)_-_1)_)
percases ( len (F | k) = 0 or len (F | k) <> 0 ) ;
supposeA9: len (F | k) = 0 ; ::_thesis: ex d being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) )
then 0 in dom F by A6, A8, CARD_1:49, TARSKI:def_1;
then A10: F . 0 in rng F by FUNCT_1:def_3;
reconsider f = NAT --> (F . 0) as Function of NAT,D by A10, FUNCOP_1:45;
take d = f . 0; ::_thesis: ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) )
take f = f; ::_thesis: ( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) )
thus f . 0 = F . 0 by FUNCOP_1:7; ::_thesis: ( ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) )
thus for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) by A6, A8, A9, NAT_1:14; ::_thesis: d = f . ((len F) - 1)
k < k + 1 by NAT_1:13;
hence d = f . ((len F) - 1) by A6, A9, AFINSQ_1:11; ::_thesis: verum
end;
supposeA11: len (F | k) <> 0 ; ::_thesis: ex a being Element of D ex h being Function of NAT,D st
( h . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
h . (n + 1) = b . ((h . n),(F . (n + 1))) ) & a = h . ((len F) - 1) )
k < len F by A6, NAT_1:13;
then k in dom F by NAT_1:44;
then A12: F . k in rng F by FUNCT_1:def_3;
reconsider d1 = F . k as Element of D by A12;
A13: 0 in len (F | k) by A11, NAT_1:44;
consider d being Element of D, f being Function of NAT,D such that
A14: f . 0 = (F | k) . 0 and
A15: for n being Nat st n + 1 < len (F | k) holds
f . (n + 1) = b . ((f . n),((F | k) . (n + 1))) and
A16: d = f . ((len (F | k)) - 1) by A5, A6, A7, A11, AFINSQ_1:11;
deffunc H1( Element of NAT ) -> Element of D = f . $1;
reconsider K = k as Element of NAT by ORDINAL1:def_12;
consider h being Function of NAT,D such that
A17: h . K = b . (d,d1) and
A18: for n being Element of NAT st n <> K holds
h . n = H1(n) from FUNCT_2:sch_6();
take a = h . k; ::_thesis: ex h being Function of NAT,D st
( h . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
h . (n + 1) = b . ((h . n),(F . (n + 1))) ) & a = h . ((len F) - 1) )
take h = h; ::_thesis: ( h . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
h . (n + 1) = b . ((h . n),(F . (n + 1))) ) & a = h . ((len F) - 1) )
h . 0 = f . 0 by A8, A11, A18;
hence h . 0 = F . 0 by A14, A13, FUNCT_1:47; ::_thesis: ( ( for n being Nat st n + 1 < len F holds
h . (n + 1) = b . ((h . n),(F . (n + 1))) ) & a = h . ((len F) - 1) )
thus for n being Nat st n + 1 < len F holds
h . (n + 1) = b . ((h . n),(F . (n + 1))) ::_thesis: a = h . ((len F) - 1)
proof
let n be Nat; ::_thesis: ( n + 1 < len F implies h . (n + 1) = b . ((h . n),(F . (n + 1))) )
assume n + 1 < len F ; ::_thesis: h . (n + 1) = b . ((h . n),(F . (n + 1)))
then A19: n + 1 <= len (F | k) by A6, A8, NAT_1:13;
now__::_thesis:_h_._(n_+_1)_=_b_._((h_._n),(F_._(n_+_1)))
percases ( n + 1 = len (F | k) or n + 1 < len (F | k) ) by A19, XXREAL_0:1;
supposeA20: n + 1 = len (F | k) ; ::_thesis: h . (n + 1) = b . ((h . n),(F . (n + 1)))
then A21: n < k by A8, NAT_1:13;
( n + 1 = k & n in NAT ) by A6, A7, A20, AFINSQ_1:11, ORDINAL1:def_12;
hence h . (n + 1) = b . ((h . n),(F . (n + 1))) by A16, A17, A18, A20, A21; ::_thesis: verum
end;
supposeA22: n + 1 < len (F | k) ; ::_thesis: h . (n + 1) = b . ((h . n),(F . (n + 1)))
then n + 1 in dom (F | k) by NAT_1:44;
then A23: (F | k) . (n + 1) = F . (n + 1) by FUNCT_1:47;
( n <= n + 1 & n in NAT ) by NAT_1:11, ORDINAL1:def_12;
then A24: f . n = h . n by A8, A18, A22;
f . (n + 1) = h . (n + 1) by A8, A18, A22;
hence h . (n + 1) = b . ((h . n),(F . (n + 1))) by A15, A22, A23, A24; ::_thesis: verum
end;
end;
end;
hence h . (n + 1) = b . ((h . n),(F . (n + 1))) ; ::_thesis: verum
end;
thus a = h . ((len F) - 1) by A6; ::_thesis: verum
end;
end;
end;
hence ex d being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d = f . ((len F) - 1) ) ; ::_thesis: verum
end;
A25: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A25, A4);
hence ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) ) by A1, A3; ::_thesis: verum
end;
end;
end;
hence ( ( b is having_a_unity & len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of D holds
( ( b is having_a_unity & len F = 0 & b1 = the_unity_wrt b & b2 = the_unity_wrt b implies b1 = b2 ) & ( ( not b is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b1 = f . ((len F) - 1) ) & ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b2 = f . ((len F) - 1) ) implies b1 = b2 ) )
proof
let d1, d2 be Element of D; ::_thesis: ( ( b is having_a_unity & len F = 0 & d1 = the_unity_wrt b & d2 = the_unity_wrt b implies d1 = d2 ) & ( ( not b is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d1 = f . ((len F) - 1) ) & ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d2 = f . ((len F) - 1) ) implies d1 = d2 ) )
thus ( b is having_a_unity & len F = 0 & d1 = the_unity_wrt b & d2 = the_unity_wrt b implies d1 = d2 ) ; ::_thesis: ( ( not b is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d1 = f . ((len F) - 1) ) & ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & d2 = f . ((len F) - 1) ) implies d1 = d2 )
A26: ((len F) - 1) + 1 = len F ;
assume ( not b is having_a_unity or len F <> 0 ) ; ::_thesis: ( for f being Function of NAT,D holds
( not f . 0 = F . 0 or ex n being Nat st
( n + 1 < len F & not f . (n + 1) = b . ((f . n),(F . (n + 1))) ) or not d1 = f . ((len F) - 1) ) or for f being Function of NAT,D holds
( not f . 0 = F . 0 or ex n being Nat st
( n + 1 < len F & not f . (n + 1) = b . ((f . n),(F . (n + 1))) ) or not d2 = f . ((len F) - 1) ) or d1 = d2 )
then 0 < len F by A2;
then A27: (len F) - 1 is Element of NAT by NAT_1:20;
given f1 being Function of NAT,D such that A28: f1 . 0 = F . 0 and
A29: for n being Nat st n + 1 < len F holds
f1 . (n + 1) = b . ((f1 . n),(F . (n + 1))) and
A30: d1 = f1 . ((len F) - 1) ; ::_thesis: ( for f being Function of NAT,D holds
( not f . 0 = F . 0 or ex n being Nat st
( n + 1 < len F & not f . (n + 1) = b . ((f . n),(F . (n + 1))) ) or not d2 = f . ((len F) - 1) ) or d1 = d2 )
given f2 being Function of NAT,D such that A31: f2 . 0 = F . 0 and
A32: for n being Nat st n + 1 < len F holds
f2 . (n + 1) = b . ((f2 . n),(F . (n + 1))) and
A33: d2 = f2 . ((len F) - 1) ; ::_thesis: d1 = d2
defpred S1[ Nat] means ( $1 + 1 <= len F implies f1 . $1 = f2 . $1 );
A34: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A35: S1[n] ; ::_thesis: S1[n + 1]
assume (n + 1) + 1 <= len F ; ::_thesis: f1 . (n + 1) = f2 . (n + 1)
then A36: n + 1 < len F by NAT_1:13;
then f2 . (n + 1) = b . ((f2 . n),(F . (n + 1))) by A32;
hence f1 . (n + 1) = f2 . (n + 1) by A29, A35, A36; ::_thesis: verum
end;
A37: S1[ 0 ] by A28, A31;
for n being Nat holds S1[n] from NAT_1:sch_2(A37, A34);
hence d1 = d2 by A30, A33, A26, A27; ::_thesis: verum
end;
consistency
for b1 being Element of D holds verum ;
end;
:: deftheorem Def8 defines "**" AFINSQ_2:def_8_:_
for D being non empty set
for F being XFinSequence st F is D -valued holds
for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds
for b4 being Element of D holds
( ( b is having_a_unity & len F = 0 implies ( b4 = b "**" F iff b4 = the_unity_wrt b ) ) & ( ( not b is having_a_unity or not len F = 0 ) implies ( b4 = b "**" F iff ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b4 = f . ((len F) - 1) ) ) ) );
theorem Th37: :: AFINSQ_2:37
for D being non empty set
for b being BinOp of D
for d being Element of D holds b "**" <%d%> = d
proof
let D be non empty set ; ::_thesis: for b being BinOp of D
for d being Element of D holds b "**" <%d%> = d
let b be BinOp of D; ::_thesis: for d being Element of D holds b "**" <%d%> = d
let d be Element of D; ::_thesis: b "**" <%d%> = d
len <%d%> = 1 by AFINSQ_1:33;
then ex f being Function of NAT,D st
( f . 0 = <%d%> . 0 & ( for n being Nat st n + 1 < len <%d%> holds
f . (n + 1) = b . ((f . n),(<%d%> . (n + 1))) ) & b "**" <%d%> = f . (1 - 1) ) by Def8;
hence b "**" <%d%> = d by AFINSQ_1:34; ::_thesis: verum
end;
theorem Th38: :: AFINSQ_2:38
for D being non empty set
for b being BinOp of D
for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2)
proof
let D be non empty set ; ::_thesis: for b being BinOp of D
for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2)
let b be BinOp of D; ::_thesis: for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2)
let d1, d2 be Element of D; ::_thesis: b "**" <%d1,d2%> = b . (d1,d2)
A1: <%d1,d2%> . 0 = d1 by AFINSQ_1:38;
len <%d1,d2%> = 2 by AFINSQ_1:38;
then consider f being Function of NAT,D such that
A2: f . 0 = <%d1,d2%> . 0 and
A3: for n being Nat st n + 1 < 2 holds
f . (n + 1) = b . ((f . n),(<%d1,d2%> . (n + 1))) and
A4: b "**" <%d1,d2%> = f . (2 - 1) by Def8;
f . (0 + 1) = b . ((f . 0),(<%d1,d2%> . (0 + 1))) by A3;
hence b "**" <%d1,d2%> = b . (d1,d2) by A2, A4, A1, AFINSQ_1:38; ::_thesis: verum
end;
theorem Th39: :: AFINSQ_2:39
for D being non empty set
for b being BinOp of D
for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2)
proof
let D be non empty set ; ::_thesis: for b being BinOp of D
for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2)
let b be BinOp of D; ::_thesis: for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2)
let d, d1, d2 be Element of D; ::_thesis: b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2)
set F = <%d,d1,d2%>;
A1: <%d,d1,d2%> . 0 = d by AFINSQ_1:39;
A2: <%d,d1,d2%> . 1 = d1 by AFINSQ_1:39;
len <%d,d1,d2%> = 3 by AFINSQ_1:39;
then consider f being Function of NAT,D such that
A3: f . 0 = <%d,d1,d2%> . 0 and
A4: for n being Nat st n + 1 < 3 holds
f . (n + 1) = b . ((f . n),(<%d,d1,d2%> . (n + 1))) and
A5: b "**" <%d,d1,d2%> = f . (3 - 1) by Def8;
A6: f . (1 + 1) = b . ((f . 1),(<%d,d1,d2%> . (1 + 1))) by A4;
f . (0 + 1) = b . ((f . 0),(<%d,d1,d2%> . (0 + 1))) by A4;
hence b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2) by A3, A5, A6, A1, A2, AFINSQ_1:39; ::_thesis: verum
end;
theorem Th40: :: AFINSQ_2:40
for D being non empty set
for F being XFinSequence of D
for b being BinOp of D
for d being Element of D st ( b is having_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . ((b "**" F),d)
proof
let D be non empty set ; ::_thesis: for F being XFinSequence of D
for b being BinOp of D
for d being Element of D st ( b is having_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . ((b "**" F),d)
let F be XFinSequence of D; ::_thesis: for b being BinOp of D
for d being Element of D st ( b is having_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . ((b "**" F),d)
let b be BinOp of D; ::_thesis: for d being Element of D st ( b is having_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . ((b "**" F),d)
let d be Element of D; ::_thesis: ( ( b is having_a_unity or len F > 0 ) implies b "**" (F ^ <%d%>) = b . ((b "**" F),d) )
assume A1: ( b is having_a_unity or len F > 0 ) ; ::_thesis: b "**" (F ^ <%d%>) = b . ((b "**" F),d)
now__::_thesis:_b_"**"_(F_^_<%d%>)_=_b_._((b_"**"_F),d)
percases ( len F < 0 + 1 or len F >= 1 ) ;
supposeA2: len F < 0 + 1 ; ::_thesis: b "**" (F ^ <%d%>) = b . ((b "**" F),d)
then A3: F = {} by NAT_1:13;
{} ^ <%d%> = <%d%> ;
then A4: b "**" (F ^ <%d%>) = d by Th37, A3;
len F = 0 by A2, NAT_1:13;
then b "**" F = the_unity_wrt b by A1, Def8;
hence b "**" (F ^ <%d%>) = b . ((b "**" F),d) by A1, A2, A4, NAT_1:13, SETWISEO:15; ::_thesis: verum
end;
supposeA5: len F >= 1 ; ::_thesis: b "**" (F ^ <%d%>) = b . ((b "**" F),d)
set G = F ^ <%d%>;
reconsider lenF1 = (len F) - 1 as Element of NAT by A5, NAT_1:21;
A6: (F ^ <%d%>) . (len F) = d by AFINSQ_1:36;
A7: len (F ^ <%d%>) = (len F) + (len <%d%>) by AFINSQ_1:17
.= (len F) + 1 by AFINSQ_1:33 ;
then 1 <= len (F ^ <%d%>) by NAT_1:12;
then consider f1 being Function of NAT,D such that
A8: f1 . 0 = (F ^ <%d%>) . 0 and
A9: for n being Nat st n + 1 < len (F ^ <%d%>) holds
f1 . (n + 1) = b . ((f1 . n),((F ^ <%d%>) . (n + 1))) and
A10: b "**" (F ^ <%d%>) = f1 . ((len (F ^ <%d%>)) - 1) by Def8;
consider f being Function of NAT,D such that
A11: f . 0 = F . 0 and
A12: for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) and
A13: b "**" F = f . ((len F) - 1) by A5, Def8;
defpred S1[ Nat] means ( $1 + 1 < len (F ^ <%d%>) implies f . $1 = f1 . $1 );
A14: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A15: S1[n] ; ::_thesis: S1[n + 1]
set n1 = n + 1;
assume A16: (n + 1) + 1 < len (F ^ <%d%>) ; ::_thesis: f . (n + 1) = f1 . (n + 1)
then n + 1 < len (F ^ <%d%>) by NAT_1:13;
then A17: f1 . (n + 1) = b . ((f1 . n),((F ^ <%d%>) . (n + 1))) by A9;
A18: ((n + 1) + 1) + (- 1) < ((len F) + 1) + (- 1) by A7, A16, XREAL_1:8;
then A19: n + 1 in len F by NAT_1:44;
f . (n + 1) = b . ((f . n),(F . (n + 1))) by A12, A18;
hence f . (n + 1) = f1 . (n + 1) by A15, A16, A17, A19, AFINSQ_1:def_3, NAT_1:13; ::_thesis: verum
end;
0 in len F by A5, NAT_1:44;
then A20: S1[ 0 ] by A11, A8, AFINSQ_1:def_3;
A21: for n being Nat holds S1[n] from NAT_1:sch_2(A20, A14);
A22: lenF1 + 1 < len (F ^ <%d%>) by A7, NAT_1:13;
then b "**" (F ^ <%d%>) = b . ((f1 . lenF1),((F ^ <%d%>) . (lenF1 + 1))) by A7, A9, A10;
hence b "**" (F ^ <%d%>) = b . ((b "**" F),d) by A13, A21, A22, A6; ::_thesis: verum
end;
end;
end;
hence b "**" (F ^ <%d%>) = b . ((b "**" F),d) ; ::_thesis: verum
end;
theorem Th41: :: AFINSQ_2:41
for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
proof
let D be non empty set ; ::_thesis: for F, G being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
let F, G be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) )
defpred S1[ XFinSequence of D] means for F being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len $1 >= 1 ) ) holds
b "**" (F ^ $1) = b . ((b "**" F),(b "**" $1));
A1: for G being XFinSequence of D
for d being Element of D st S1[G] holds
S1[G ^ <%d%>]
proof
let G be XFinSequence of D; ::_thesis: for d being Element of D st S1[G] holds
S1[G ^ <%d%>]
let d be Element of D; ::_thesis: ( S1[G] implies S1[G ^ <%d%>] )
assume A2: S1[G] ; ::_thesis: S1[G ^ <%d%>]
let F be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) holds
b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))
let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) implies b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) )
assume that
A3: b is associative and
A4: ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))
now__::_thesis:_b_"**"_(F_^_(G_^_<%d%>))_=_b_._((b_"**"_F),(b_"**"_(G_^_<%d%>)))
percases ( len G <> 0 or len G = 0 ) ;
supposeA5: len G <> 0 ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))
then ( b is having_a_unity or ( len F >= 1 & len (F ^ G) = (len F) + (len G) & (len F) + (len G) > (len F) + 0 ) ) by A4, AFINSQ_1:17, XREAL_1:8;
then b . ((b "**" (F ^ G)),d) = b "**" ((F ^ G) ^ <%d%>) by Th40;
then A6: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" (F ^ G)),d) by AFINSQ_1:27;
len G >= 1 by A5, NAT_1:14;
then b "**" (F ^ (G ^ <%d%>)) = b . ((b . ((b "**" F),(b "**" G))),d) by A2, A3, A4, A6
.= b . ((b "**" F),(b . ((b "**" G),d))) by A3, BINOP_1:def_3
.= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A5, Th40 ;
hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; ::_thesis: verum
end;
suppose len G = 0 ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))
then A7: G = {} ;
hence b "**" (F ^ (G ^ <%d%>)) = b "**" (F ^ ({} ^ <%d%>))
.= b "**" (F ^ <%d%>)
.= b . ((b "**" F),d) by A4, Th40
.= b . ((b "**" F),(b "**" ({} ^ <%d%>))) by Th37
.= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A7 ;
::_thesis: verum
end;
end;
end;
hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; ::_thesis: verum
end;
A8: S1[ <%> D]
proof
let F be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) holds
b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D)))
let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) implies b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D))) )
assume that
b is associative and
A9: ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) ; ::_thesis: b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D)))
thus b "**" (F ^ (<%> D)) = b "**" (F ^ {})
.= b . ((b "**" F),(the_unity_wrt b)) by A9, SETWISEO:15
.= b . ((b "**" F),(b "**" (<%> D))) by A9, Def8, CARD_1:27 ; ::_thesis: verum
end;
for G being XFinSequence of D holds S1[G] from AFINSQ_2:sch_2(A8, A1);
hence ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) ) ; ::_thesis: verum
end;
theorem Th42: :: AFINSQ_2:42
for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
proof
let D be non empty set ; ::_thesis: for F, G being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
let F, G be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) )
defpred S1[ XFinSequence of D] means for F being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len $1 >= 1 ) ) holds
b "**" (F ^ $1) = b . ((b "**" F),(b "**" $1));
A1: for G being XFinSequence of D
for d being Element of D st S1[G] holds
S1[G ^ <%d%>]
proof
let G be XFinSequence of D; ::_thesis: for d being Element of D st S1[G] holds
S1[G ^ <%d%>]
let d be Element of D; ::_thesis: ( S1[G] implies S1[G ^ <%d%>] )
assume A2: S1[G] ; ::_thesis: S1[G ^ <%d%>]
let F be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) holds
b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))
let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) implies b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) )
assume that
A3: b is associative and
A4: ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))
now__::_thesis:_b_"**"_(F_^_(G_^_<%d%>))_=_b_._((b_"**"_F),(b_"**"_(G_^_<%d%>)))
percases ( len G <> 0 or len G = 0 ) ;
supposeA5: len G <> 0 ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))
then ( b is having_a_unity or ( len F >= 1 & len (F ^ G) = (len F) + (len G) & (len F) + (len G) > (len F) + 0 ) ) by A4, AFINSQ_1:17, XREAL_1:8;
then b . ((b "**" (F ^ G)),d) = b "**" ((F ^ G) ^ <%d%>) by Th40;
then A6: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" (F ^ G)),d) by AFINSQ_1:27;
len G >= 1 by A5, NAT_1:14;
then b "**" (F ^ (G ^ <%d%>)) = b . ((b . ((b "**" F),(b "**" G))),d) by A2, A3, A4, A6
.= b . ((b "**" F),(b . ((b "**" G),d))) by A3, BINOP_1:def_3
.= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A5, Th40 ;
hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; ::_thesis: verum
end;
suppose len G = 0 ; ::_thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))
then A7: G = {} ;
hence b "**" (F ^ (G ^ <%d%>)) = b "**" (F ^ ({} ^ <%d%>))
.= b "**" (F ^ <%d%>)
.= b . ((b "**" F),d) by A4, Th40
.= b . ((b "**" F),(b "**" ({} ^ <%d%>))) by Th37
.= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A7 ;
::_thesis: verum
end;
end;
end;
hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; ::_thesis: verum
end;
A8: S1[ <%> D]
proof
let F be XFinSequence of D; ::_thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) holds
b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D)))
let b be BinOp of D; ::_thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) implies b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D))) )
assume that
b is associative and
A9: ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) ; ::_thesis: b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D)))
thus b "**" (F ^ (<%> D)) = b "**" (F ^ {})
.= b . ((b "**" F),(the_unity_wrt b)) by A9, SETWISEO:15
.= b . ((b "**" F),(b "**" (<%> D))) by A9, Def8, CARD_1:27 ; ::_thesis: verum
end;
for G being XFinSequence of D holds S1[G] from AFINSQ_2:sch_2(A8, A1);
hence ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) ) ; ::_thesis: verum
end;
theorem Th43: :: AFINSQ_2:43
for n being Nat
for D being non empty set
for F being XFinSequence of D
for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
proof
let n be Nat; ::_thesis: for D being non empty set
for F being XFinSequence of D
for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
let D be non empty set ; ::_thesis: for F being XFinSequence of D
for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
let F be XFinSequence of D; ::_thesis: for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
let b be BinOp of D; ::_thesis: ( n in dom F & ( b is having_a_unity or n <> 0 ) implies b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) )
assume that
A1: n in dom F and
A2: ( b is having_a_unity or n <> 0 ) ; ::_thesis: b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
len F > n by A1, NAT_1:44;
then A3: len (F | n) = n by AFINSQ_1:54;
defpred S1[ Nat] means ( $1 in dom F & ( b is having_a_unity or len (F | $1) >= 1 ) implies b . ((b "**" (F | $1)),(F . $1)) = b "**" (F | ($1 + 1)) );
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
set k1 = k + 1;
set Fk1 = F | (k + 1);
set Fk2 = F | ((k + 1) + 1);
assume that
A5: k + 1 in dom F and
A6: ( b is having_a_unity or len (F | (k + 1)) >= 1 ) ; ::_thesis: b . ((b "**" (F | (k + 1))),(F . (k + 1))) = b "**" (F | ((k + 1) + 1))
A7: 0 in dom F by A5, NAT_1:44;
0 in k + 1 by NAT_1:44;
then 0 in (dom F) /\ (k + 1) by A7, XBOOLE_0:def_4;
then 0 in dom (F | (k + 1)) by RELAT_1:61;
then A8: (F | (k + 1)) . 0 = F . 0 by FUNCT_1:47;
A9: k < k + 1 by NAT_1:13;
k + 1 < (k + 1) + 1 by NAT_1:13;
then k + 1 in (k + 1) + 1 by NAT_1:44;
then A10: k + 1 in (dom F) /\ ((k + 1) + 1) by A5, XBOOLE_0:def_4;
A11: dom F = len F ;
A12: k + 1 < dom F by A5, NAT_1:44;
then A13: len (F | (k + 1)) = k + 1 by A11, AFINSQ_1:54;
then consider f1 being Function of NAT,D such that
A14: f1 . 0 = (F | (k + 1)) . 0 and
A15: for n being Nat st n + 1 < len (F | (k + 1)) holds
f1 . (n + 1) = b . ((f1 . n),((F | (k + 1)) . (n + 1))) and
A16: b "**" (F | (k + 1)) = f1 . ((k + 1) - 1) by A6, Def8;
(k + 1) + 1 <= dom F by A12, NAT_1:13;
then A17: len (F | ((k + 1) + 1)) = (k + 1) + 1 by A11, AFINSQ_1:54;
then ( b is having_a_unity or len (F | ((k + 1) + 1)) >= 1 ) by A6, A13, NAT_1:13;
then consider f2 being Function of NAT,D such that
A18: f2 . 0 = (F | ((k + 1) + 1)) . 0 and
A19: for n being Nat st n + 1 < len (F | ((k + 1) + 1)) holds
f2 . (n + 1) = b . ((f2 . n),((F | ((k + 1) + 1)) . (n + 1))) and
A20: b "**" (F | ((k + 1) + 1)) = f2 . (((k + 1) + 1) - 1) by A17, Def8;
defpred S2[ Nat] means ( $1 < k + 1 implies f1 . $1 = f2 . $1 );
A21: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] )
assume A22: S2[m] ; ::_thesis: S2[m + 1]
set m1 = m + 1;
assume A23: m + 1 < k + 1 ; ::_thesis: f1 . (m + 1) = f2 . (m + 1)
k + 1 < dom F by A5, NAT_1:44;
then m + 1 < dom F by A23, XXREAL_0:2;
then A24: m + 1 in dom F by NAT_1:44;
m + 1 < (k + 1) + 1 by A23, NAT_1:13;
then m + 1 in (k + 1) + 1 by NAT_1:44;
then m + 1 in (dom F) /\ ((k + 1) + 1) by A24, XBOOLE_0:def_4;
then m + 1 in dom (F | ((k + 1) + 1)) by RELAT_1:61;
then A25: (F | ((k + 1) + 1)) . (m + 1) = F . (m + 1) by FUNCT_1:47;
m + 1 in k + 1 by A23, NAT_1:44;
then m + 1 in (dom F) /\ (k + 1) by A24, XBOOLE_0:def_4;
then m + 1 in dom (F | (k + 1)) by RELAT_1:61;
then A26: (F | (k + 1)) . (m + 1) = F . (m + 1) by FUNCT_1:47;
m + 1 < len (F | ((k + 1) + 1)) by A17, A23, NAT_1:13;
then f2 . (m + 1) = b . ((f1 . m),((F | (k + 1)) . (m + 1))) by A19, A22, A23, A26, A25, NAT_1:13;
hence f1 . (m + 1) = f2 . (m + 1) by A13, A15, A23; ::_thesis: verum
end;
0 in (k + 1) + 1 by NAT_1:44;
then 0 in (dom F) /\ ((k + 1) + 1) by A7, XBOOLE_0:def_4;
then 0 in dom (F | ((k + 1) + 1)) by RELAT_1:61;
then A27: S2[ 0 ] by A14, A18, A8, FUNCT_1:47;
for m being Nat holds S2[m] from NAT_1:sch_2(A27, A21);
then A28: ( (dom F) /\ ((k + 1) + 1) = dom (F | ((k + 1) + 1)) & f1 . k = f2 . k ) by A9, RELAT_1:61;
k + 1 < (k + 1) + 1 by NAT_1:13;
then f2 . (k + 1) = b . ((f2 . k),((F | ((k + 1) + 1)) . (k + 1))) by A17, A19;
hence b . ((b "**" (F | (k + 1))),(F . (k + 1))) = b "**" (F | ((k + 1) + 1)) by A16, A20, A10, A28, FUNCT_1:47; ::_thesis: verum
end;
A29: S1[ 0 ]
proof
assume that
A30: 0 in dom F and
A31: ( b is having_a_unity or len (F | 0) >= 1 ) ; ::_thesis: b . ((b "**" (F | 0)),(F . 0)) = b "**" (F | (0 + 1))
A32: F . 0 in rng F by A30, FUNCT_1:def_3;
len F > 0 by A30;
then A33: len (F | 1) = 1 by AFINSQ_1:54, NAT_1:14;
then A34: F | 1 = <%((F | 1) . 0)%> by AFINSQ_1:34;
0 in 1 by NAT_1:44;
then A35: F . 0 = (F | 1) . 0 by A33, FUNCT_1:47;
len (F | 0) = 0 ;
then b "**" (F | 0) = the_unity_wrt b by A31, Def8;
then b . ((b "**" (F | 0)),(F . 0)) = F . 0 by A31, A32, SETWISEO:15;
hence b . ((b "**" (F | 0)),(F . 0)) = b "**" (F | (0 + 1)) by A32, A34, A35, Th37; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A29, A4);
hence b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) by A1, A2, A3, NAT_1:14; ::_thesis: verum
end;
theorem Th44: :: AFINSQ_2:44
for D being non empty set
for F being XFinSequence of D
for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds
b "**" F = b "**" (XFS2FS F)
proof
let D be non empty set ; ::_thesis: for F being XFinSequence of D
for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds
b "**" F = b "**" (XFS2FS F)
let F be XFinSequence of D; ::_thesis: for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds
b "**" F = b "**" (XFS2FS F)
let b be BinOp of D; ::_thesis: ( ( b is having_a_unity or len F >= 1 ) implies b "**" F = b "**" (XFS2FS F) )
assume A1: ( b is having_a_unity or len F >= 1 ) ; ::_thesis: b "**" F = b "**" (XFS2FS F)
percases ( len F >= 1 or ( b is having_a_unity & len F < 1 ) ) by A1;
supposeA2: len F >= 1 ; ::_thesis: b "**" F = b "**" (XFS2FS F)
set FS = XFS2FS F;
len F = len (XFS2FS F) by AFINSQ_1:def_9;
then consider f being Function of NAT,D such that
A3: f . 1 = (XFS2FS F) . 1 and
A4: for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = b . ((f . n),((XFS2FS F) . (n + 1))) and
A5: b "**" (XFS2FS F) = f . (len F) by A2, FINSOP_1:def_1;
consider xf being Function of NAT,D such that
A6: xf . 0 = F . 0 and
A7: for n being Nat st n + 1 < len F holds
xf . (n + 1) = b . ((xf . n),(F . (n + 1))) and
A8: b "**" F = xf . ((len F) - 1) by A2, Def8;
defpred S1[ Nat] means ( $1 < len F implies xf . $1 = f . ($1 + 1) );
A9: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A10: S1[n] ; ::_thesis: S1[n + 1]
set n1 = n + 1;
set n2 = (n + 1) + 1;
assume A11: n + 1 < len F ; ::_thesis: xf . (n + 1) = f . ((n + 1) + 1)
then ( 0 + 1 <= (n + 1) + 1 & (n + 1) + 1 <= len F ) by NAT_1:13;
then A12: F . (((n + 1) + 1) -' 1) = (XFS2FS F) . ((n + 1) + 1) by AFINSQ_1:def_9;
( xf . (n + 1) = b . ((xf . n),(F . (n + 1))) & f . ((n + 1) + 1) = b . ((f . (n + 1)),((XFS2FS F) . ((n + 1) + 1))) ) by A7, A4, A11;
hence xf . (n + 1) = f . ((n + 1) + 1) by A10, A11, A12, NAT_1:13, NAT_D:34; ::_thesis: verum
end;
reconsider L1 = (len F) - 1 as Element of NAT by A2, NAT_1:21;
A13: L1 < L1 + 1 by NAT_1:13;
A14: S1[ 0 ]
proof
assume 0 < len F ; ::_thesis: xf . 0 = f . (0 + 1)
then 0 + 1 <= len F by NAT_1:13;
then F . (1 -' 1) = (XFS2FS F) . 1 by AFINSQ_1:def_9;
hence xf . 0 = f . (0 + 1) by A6, A3, XREAL_1:232; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A14, A9);
hence b "**" F = b "**" (XFS2FS F) by A8, A5, A13; ::_thesis: verum
end;
supposeA15: ( b is having_a_unity & len F < 1 ) ; ::_thesis: b "**" F = b "**" (XFS2FS F)
then len F <= 0 + 1 ;
then A16: len F = 0 by A15, NAT_1:8;
then ( len F = len (XFS2FS F) & b "**" F = the_unity_wrt b ) by A15, Def8, AFINSQ_1:def_9;
hence b "**" F = b "**" (XFS2FS F) by A15, A16, FINSOP_1:def_1; ::_thesis: verum
end;
end;
end;
theorem Th45: :: AFINSQ_2:45
for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D
for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds
b "**" F = b "**" G
proof
let D be non empty set ; ::_thesis: for F, G being XFinSequence of D
for b being BinOp of D
for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds
b "**" F = b "**" G
let F, G be XFinSequence of D; ::_thesis: for b being BinOp of D
for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds
b "**" F = b "**" G
let b be BinOp of D; ::_thesis: for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds
b "**" F = b "**" G
let P be Permutation of (dom F); ::_thesis: ( b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P implies b "**" F = b "**" G )
assume that
A1: ( b is commutative & b is associative ) and
A2: ( b is having_a_unity or len F >= 1 ) and
A3: G = F * P ; ::_thesis: b "**" F = b "**" G
set xF = XFS2FS F;
A4: ( b is having_a_unity or len (XFS2FS F) >= 1 ) by A2, AFINSQ_1:def_9;
set xG = XFS2FS G;
defpred S1[ set , set ] means for n being Nat st $1 = n holds
$2 = (P . (n - 1)) + 1;
dom F = len F ;
then reconsider d = dom F as Element of NAT ;
A5: for x being set st x in Seg d holds
ex y being set st
( y in Seg d & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Seg d implies ex y being set st
( y in Seg d & S1[x,y] ) )
assume A6: x in Seg d ; ::_thesis: ex y being set st
( y in Seg d & S1[x,y] )
reconsider x9 = x as Element of NAT by A6;
1 + 0 <= x9 by A6, FINSEQ_1:1;
then reconsider x91 = x9 - 1 as Element of NAT by NAT_1:21;
A7: x91 + 1 <= d by A6, FINSEQ_1:1;
then x91 < d by NAT_1:13;
then A8: x91 in d by NAT_1:44;
take (P . x91) + 1 ; ::_thesis: ( (P . x91) + 1 in Seg d & S1[x,(P . x91) + 1] )
dom F = dom P by A7, FUNCT_2:def_1;
then P . x91 in rng P by A8, FUNCT_1:def_3;
then P . x91 < d by NAT_1:44;
then ( 0 + 1 <= (P . x91) + 1 & (P . x91) + 1 <= d ) by NAT_1:13;
hence ( (P . x91) + 1 in Seg d & S1[x,(P . x91) + 1] ) by FINSEQ_1:1; ::_thesis: verum
end;
consider P9 being Function of (Seg d),(Seg d) such that
A9: for x being set st x in Seg d holds
S1[x,P9 . x] from FUNCT_2:sch_1(A5);
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_P9_&_x2_in_dom_P9_&_P9_._x1_=_P9_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom P9 & x2 in dom P9 & P9 . x1 = P9 . x2 implies x1 = x2 )
assume that
A10: x1 in dom P9 and
A11: x2 in dom P9 and
A12: P9 . x1 = P9 . x2 ; ::_thesis: x1 = x2
dom P9 = Seg d by FUNCT_2:52;
then reconsider X1 = x1, X2 = x2 as Element of NAT by A10, A11;
( 1 + 0 <= X1 & 1 + 0 <= X2 ) by A10, A11, FINSEQ_1:1;
then reconsider X19 = X1 - 1, X29 = X2 - 1 as Element of NAT by NAT_1:21;
A13: ( X19 < X19 + 1 & X1 <= d ) by A10, FINSEQ_1:1, NAT_1:13;
then A14: dom P = dom F by FUNCT_2:def_1;
( X29 < X29 + 1 & X2 <= d ) by A11, FINSEQ_1:1, NAT_1:13;
then X29 < d by XXREAL_0:2;
then A15: X29 in dom P by A14, NAT_1:44;
X19 < d by A13, XXREAL_0:2;
then A16: X19 in dom P by A14, NAT_1:44;
P9 . X1 = (P . X19) + 1 by A9, A10;
then ((P . X19) + 1) - 1 = ((P . X29) + 1) - 1 by A9, A11, A12;
then (X1 - 1) + 1 = (X2 - 1) + 1 by A16, A15, FUNCT_1:def_4;
hence x1 = x2 ; ::_thesis: verum
end;
then A17: P9 is one-to-one by FUNCT_1:def_4;
card (Seg d) = card (Seg d) ;
then A18: ( P9 is one-to-one & P9 is onto ) by A17, Lm2;
len (XFS2FS F) = len F by AFINSQ_1:def_9;
then dom (XFS2FS F) = Seg (len F) by FINSEQ_1:def_3;
then reconsider P9 = P9 as Permutation of (dom (XFS2FS F)) by A18;
A19: ( dom P9 = Seg d & dom (XFS2FS G) = Seg (len (XFS2FS G)) ) by FINSEQ_1:def_3, FUNCT_2:52;
rng P9 c= dom (XFS2FS F) ;
then A20: dom ((XFS2FS F) * P9) = dom P9 by RELAT_1:27;
rng P c= dom F ;
then dom (F * P) = dom P by RELAT_1:27;
then A21: dom G = dom F by A3, FUNCT_2:52;
A22: dom G = len G ;
A23: for x9 being set st x9 in dom (XFS2FS G) holds
(XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9
proof
let x9 be set ; ::_thesis: ( x9 in dom (XFS2FS G) implies (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 )
assume A24: x9 in dom (XFS2FS G) ; ::_thesis: (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9
reconsider x = x9 as Element of NAT by A24;
A25: dom (XFS2FS G) = Seg (len (XFS2FS G)) by FINSEQ_1:def_3;
then A26: 1 <= x by A24, FINSEQ_1:1;
then A27: x -' 1 = x - 1 by XREAL_1:233;
0 < x by A24, A25, FINSEQ_1:1;
then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
A28: dom (XFS2FS F) = Seg (len (XFS2FS F)) by FINSEQ_1:def_3;
A29: len (XFS2FS G) = len G by AFINSQ_1:def_9;
then A30: ( (P . (x - 1)) + 1 = P9 . x & x in dom P9 ) by A9, A21, A24, A25, FUNCT_2:52;
then A31: (P . (x - 1)) + 1 in rng P9 by FUNCT_1:def_3;
A32: x <= len F by A21, A24, A25, A29, FINSEQ_1:1;
then A33: (XFS2FS G) . x = (F * P) . (x -' 1) by A3, A21, A22, A26, AFINSQ_1:def_9;
len (XFS2FS F) = len F by AFINSQ_1:def_9;
then A34: (P . (x - 1)) + 1 <= len F by A31, A28, FINSEQ_1:1;
( x1 < x1 + 1 & x -' 1 = x1 ) by A26, NAT_1:13, XREAL_1:233;
then x -' 1 < dom G by A21, A32, XXREAL_0:2;
then x -' 1 in dom G by NAT_1:44;
then A35: ( ((P . (x -' 1)) + 1) -' 1 = P . (x -' 1) & (F * P) . (x -' 1) = F . (P . (x -' 1)) ) by A3, FUNCT_1:12, NAT_D:34;
1 <= (P . (x - 1)) + 1 by A31, A28, FINSEQ_1:1;
then (F * P) . (x -' 1) = (XFS2FS F) . ((P . (x - 1)) + 1) by A34, A27, A35, AFINSQ_1:def_9;
hence (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 by A30, A33, FUNCT_1:13; ::_thesis: verum
end;
len (XFS2FS G) = len F by A21, A22, AFINSQ_1:def_9;
then XFS2FS G = (XFS2FS F) * P9 by A23, A20, A19, FUNCT_1:def_11;
then A36: b "**" (XFS2FS G) = b "**" (XFS2FS F) by A1, A4, FINSOP_1:7;
b "**" (XFS2FS G) = b "**" G by A2, A21, A22, Th44;
hence b "**" F = b "**" G by A2, A36, Th44; ::_thesis: verum
end;
theorem :: AFINSQ_2:46
for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D
for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) holds
b "**" (F ^ G) = b "**" bFG
proof
let D be non empty set ; ::_thesis: for F, G being XFinSequence of D
for b being BinOp of D
for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) holds
b "**" (F ^ G) = b "**" bFG
let F, G be XFinSequence of D; ::_thesis: for b being BinOp of D
for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) holds
b "**" (F ^ G) = b "**" bFG
let b be BinOp of D; ::_thesis: for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) holds
b "**" (F ^ G) = b "**" bFG
let bFG be XFinSequence of D; ::_thesis: ( b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) implies b "**" (F ^ G) = b "**" bFG )
assume that
A1: ( b is commutative & b is associative ) and
A2: ( b is having_a_unity or len F >= 1 ) and
A3: len F = len G and
A4: len F = len bFG and
A5: for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ; ::_thesis: b "**" (F ^ G) = b "**" bFG
set xG = XFS2FS G;
set xF = XFS2FS F;
A6: ( b "**" F = b "**" (XFS2FS F) & b "**" G = b "**" (XFS2FS G) ) by A2, A3, Th44;
set xb = XFS2FS bFG;
A7: len (XFS2FS bFG) = len bFG by AFINSQ_1:def_9;
A8: for k being Element of NAT st k in dom (XFS2FS bFG) holds
(XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k))
proof
let k be Element of NAT ; ::_thesis: ( k in dom (XFS2FS bFG) implies (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k)) )
assume A9: k in dom (XFS2FS bFG) ; ::_thesis: (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k))
k in Seg (len (XFS2FS bFG)) by A9, FINSEQ_1:def_3;
then k >= 1 by FINSEQ_1:1;
then reconsider k1 = k - 1 as Element of NAT by NAT_1:21;
A10: k in Seg (len (XFS2FS bFG)) by A9, FINSEQ_1:def_3;
then A11: 1 <= k by FINSEQ_1:1;
then A12: k1 = k -' 1 by XREAL_1:233;
k in Seg (len (XFS2FS bFG)) by A9, FINSEQ_1:def_3;
then ( k1 < k1 + 1 & k <= len (XFS2FS bFG) ) by FINSEQ_1:1, NAT_1:13;
then k1 < len (XFS2FS bFG) by XXREAL_0:2;
then k1 in dom bFG by A7, NAT_1:44;
then A13: bFG . k1 = b . ((F . k1),(G . k1)) by A5;
A14: k <= len bFG by A7, A10, FINSEQ_1:1;
then ( bFG . (k -' 1) = (XFS2FS bFG) . k & F . (k -' 1) = (XFS2FS F) . k ) by A4, A11, AFINSQ_1:def_9;
hence (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k)) by A3, A4, A11, A14, A13, A12, AFINSQ_1:def_9; ::_thesis: verum
end;
( len (XFS2FS F) = len F & len G = len (XFS2FS G) ) by AFINSQ_1:def_9;
then b "**" (XFS2FS bFG) = b . ((b "**" (XFS2FS F)),(b "**" (XFS2FS G))) by A1, A2, A3, A4, A7, A8, FINSOP_1:9;
then b "**" bFG = b . ((b "**" F),(b "**" G)) by A2, A4, A6, Th44;
hence b "**" (F ^ G) = b "**" bFG by A1, A2, A3, Th42; ::_thesis: verum
end;
theorem Th47: :: AFINSQ_2:47
for D being non empty set
for F being XFinSequence of D
for D1, D2 being non empty set
for b1 being BinOp of D1
for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
proof
let D be non empty set ; ::_thesis: for F being XFinSequence of D
for D1, D2 being non empty set
for b1 being BinOp of D1
for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
let F be XFinSequence of D; ::_thesis: for D1, D2 being non empty set
for b1 being BinOp of D1
for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
let D1, D2 be non empty set ; ::_thesis: for b1 being BinOp of D1
for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
let b1 be BinOp of D1; ::_thesis: for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
let b2 be BinOp of D2; ::_thesis: ( len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) implies b1 "**" F = b2 "**" F )
assume that
A1: len F >= 1 and
A2: D c= D1 /\ D2 and
A3: for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ; ::_thesis: b1 "**" F = b2 "**" F
( D1 /\ D2 c= D1 & D1 /\ D2 c= D2 ) by XBOOLE_1:17;
then A4: ( D c= D1 & D c= D2 ) by A2, XBOOLE_1:1;
( rng F c= D1 & rng F c= D2 ) by A4, XBOOLE_1:1;
then A5: ( F is D1 -valued & F is D2 -valued ) by RELAT_1:def_19;
then consider F1 being Function of NAT,D1 such that
A6: F1 . 0 = F . 0 and
A7: for n being Nat st n + 1 < len F holds
F1 . (n + 1) = b1 . ((F1 . n),(F . (n + 1))) and
A8: b1 "**" F = F1 . ((len F) - 1) by A1, Def8;
consider F2 being Function of NAT,D2 such that
A9: F2 . 0 = F . 0 and
A10: for n being Nat st n + 1 < len F holds
F2 . (n + 1) = b2 . ((F2 . n),(F . (n + 1))) and
A11: b2 "**" F = F2 . ((len F) - 1) by A1, Def8, A5;
defpred S1[ Nat] means ( $1 < len F implies ( F1 . $1 = F2 . $1 & F1 . $1 in D ) );
0 in dom F by A1, NAT_1:44;
then F . 0 in rng F by FUNCT_1:def_3;
then A12: S1[ 0 ] by A6, A9;
A13: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A14: S1[n] ; ::_thesis: S1[n + 1]
assume A15: n + 1 < len F ; ::_thesis: ( F1 . (n + 1) = F2 . (n + 1) & F1 . (n + 1) in D )
then ( n + 1 in dom F & n < len F ) by NAT_1:13, NAT_1:44;
then A16: ( F . (n + 1) in rng F & n in dom F ) by FUNCT_1:def_3, NAT_1:44;
A17: F1 . (n + 1) = b1 . ((F1 . n),(F . (n + 1))) by A7, A15;
then F1 . (n + 1) = b2 . ((F2 . n),(F . (n + 1))) by A3, A16, A14, NAT_1:44
.= F2 . (n + 1) by A10, A15 ;
hence ( F1 . (n + 1) = F2 . (n + 1) & F1 . (n + 1) in D ) by A16, A14, A17, A3, NAT_1:44; ::_thesis: verum
end;
reconsider l1 = (len F) - 1 as Element of NAT by A1, NAT_1:21;
A18: l1 < l1 + 1 by NAT_1:13;
for n being Nat holds S1[n] from NAT_1:sch_2(A12, A13);
hence b1 "**" F = b2 "**" F by A8, A11, A18; ::_thesis: verum
end;
Lm3: for cF being complex-valued XFinSequence holds cF is COMPLEX -valued
proof
let cF be complex-valued XFinSequence; ::_thesis: cF is COMPLEX -valued
rng cF c= COMPLEX by VALUED_0:def_1;
hence cF is COMPLEX -valued by RELAT_1:def_19; ::_thesis: verum
end;
Lm4: for rF being real-valued XFinSequence holds rF is REAL -valued
proof
let rF be real-valued XFinSequence; ::_thesis: rF is REAL -valued
rng rF c= REAL by VALUED_0:def_3;
hence rF is REAL -valued by RELAT_1:def_19; ::_thesis: verum
end;
definition
let F be XFinSequence;
func Sum F -> Element of COMPLEX equals :: AFINSQ_2:def 9
addcomplex "**" F;
coherence
addcomplex "**" F is Element of COMPLEX ;
end;
:: deftheorem defines Sum AFINSQ_2:def_9_:_
for F being XFinSequence holds Sum F = addcomplex "**" F;
registration
let f be empty complex-valued XFinSequence;
cluster Sum f -> zero ;
coherence
Sum f is empty
proof
( f is COMPLEX -valued & len f = 0 ) by Lm3;
hence Sum f is empty by Def8, BINOP_2:1; ::_thesis: verum
end;
end;
theorem Th48: :: AFINSQ_2:48
for F being XFinSequence st F is real-valued holds
Sum F = addreal "**" F
proof
let F be XFinSequence; ::_thesis: ( F is real-valued implies Sum F = addreal "**" F )
assume A1: F is real-valued ; ::_thesis: Sum F = addreal "**" F
then rng F c= REAL by VALUED_0:def_3;
then A2: F is REAL -valued by RELAT_1:def_19;
rng F c= COMPLEX by A1, MEMBERED:1;
then A3: F is COMPLEX -valued by RELAT_1:def_19;
percases ( len F = 0 or len F >= 1 ) by NAT_1:14;
supposeA4: len F = 0 ; ::_thesis: Sum F = addreal "**" F
hence addreal "**" F = 0 by Def8, A2, BINOP_2:2
.= Sum F by Def8, A3, A4, BINOP_2:1 ;
::_thesis: verum
end;
supposeA5: len F >= 1 ; ::_thesis: Sum F = addreal "**" F
A6: REAL = REAL /\ COMPLEX by MEMBERED:1, XBOOLE_1:28;
now__::_thesis:_for_x,_y_being_set_st_x_in_REAL_&_y_in_REAL_holds_
(_addreal_._(x,y)_=_addcomplex_._(x,y)_&_addreal_._(x,y)_in_REAL_)
let x, y be set ; ::_thesis: ( x in REAL & y in REAL implies ( addreal . (x,y) = addcomplex . (x,y) & addreal . (x,y) in REAL ) )
assume ( x in REAL & y in REAL ) ; ::_thesis: ( addreal . (x,y) = addcomplex . (x,y) & addreal . (x,y) in REAL )
then reconsider X = x, Y = y as Element of REAL ;
addreal . (x,y) = X + Y by BINOP_2:def_9;
hence ( addreal . (x,y) = addcomplex . (x,y) & addreal . (x,y) in REAL ) by BINOP_2:def_3; ::_thesis: verum
end;
hence Sum F = addreal "**" F by Th47, A5, A6, A2; ::_thesis: verum
end;
end;
end;
theorem Th49: :: AFINSQ_2:49
for F being XFinSequence st F is RAT -valued holds
Sum F = addrat "**" F
proof
let F be XFinSequence; ::_thesis: ( F is RAT -valued implies Sum F = addrat "**" F )
assume A1: F is RAT -valued ; ::_thesis: Sum F = addrat "**" F
rng F c= COMPLEX by A1, MEMBERED:1;
then A2: F is COMPLEX -valued by RELAT_1:def_19;
percases ( len F = 0 or len F >= 1 ) by NAT_1:14;
supposeA3: len F = 0 ; ::_thesis: Sum F = addrat "**" F
hence addrat "**" F = 0 by Def8, A1, BINOP_2:3
.= Sum F by Def8, A2, A3, BINOP_2:1 ;
::_thesis: verum
end;
supposeA4: len F >= 1 ; ::_thesis: Sum F = addrat "**" F
A5: RAT = RAT /\ COMPLEX by MEMBERED:1, XBOOLE_1:28;
now__::_thesis:_for_x,_y_being_set_st_x_in_RAT_&_y_in_RAT_holds_
(_addrat_._(x,y)_=_addcomplex_._(x,y)_&_addrat_._(x,y)_in_RAT_)
let x, y be set ; ::_thesis: ( x in RAT & y in RAT implies ( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT ) )
assume ( x in RAT & y in RAT ) ; ::_thesis: ( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT )
then reconsider X = x, Y = y as Element of RAT ;
addrat . (x,y) = X + Y by BINOP_2:def_15;
hence ( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT ) by BINOP_2:def_3; ::_thesis: verum
end;
hence Sum F = addrat "**" F by Th47, A4, A5, A1; ::_thesis: verum
end;
end;
end;
theorem Th50: :: AFINSQ_2:50
for F being XFinSequence st F is INT -valued holds
Sum F = addint "**" F
proof
let F be XFinSequence; ::_thesis: ( F is INT -valued implies Sum F = addint "**" F )
assume A1: F is INT -valued ; ::_thesis: Sum F = addint "**" F
rng F c= COMPLEX by A1, MEMBERED:1;
then A2: F is COMPLEX -valued by RELAT_1:def_19;
percases ( len F = 0 or len F >= 1 ) by NAT_1:14;
supposeA3: len F = 0 ; ::_thesis: Sum F = addint "**" F
hence addint "**" F = 0 by Def8, A1, BINOP_2:4
.= Sum F by Def8, A2, A3, BINOP_2:1 ;
::_thesis: verum
end;
supposeA4: len F >= 1 ; ::_thesis: Sum F = addint "**" F
A5: INT = INT /\ COMPLEX by MEMBERED:1, XBOOLE_1:28;
now__::_thesis:_for_x,_y_being_set_st_x_in_INT_&_y_in_INT_holds_
(_addint_._(x,y)_=_addcomplex_._(x,y)_&_addint_._(x,y)_in_INT_)
let x, y be set ; ::_thesis: ( x in INT & y in INT implies ( addint . (x,y) = addcomplex . (x,y) & addint . (x,y) in INT ) )
assume ( x in INT & y in INT ) ; ::_thesis: ( addint . (x,y) = addcomplex . (x,y) & addint . (x,y) in INT )
then reconsider X = x, Y = y as Element of INT ;
addint . (x,y) = X + Y by BINOP_2:def_20;
hence ( addint . (x,y) = addcomplex . (x,y) & addint . (x,y) in INT ) by BINOP_2:def_3; ::_thesis: verum
end;
hence Sum F = addint "**" F by Th47, A4, A5, A1; ::_thesis: verum
end;
end;
end;
theorem Th51: :: AFINSQ_2:51
for F being XFinSequence st F is natural-valued holds
Sum F = addnat "**" F
proof
let F be XFinSequence; ::_thesis: ( F is natural-valued implies Sum F = addnat "**" F )
assume A1: F is natural-valued ; ::_thesis: Sum F = addnat "**" F
then rng F c= NAT by VALUED_0:def_6;
then A2: F is NAT -valued by RELAT_1:def_19;
rng F c= COMPLEX by A1, MEMBERED:1;
then A3: F is COMPLEX -valued by RELAT_1:def_19;
percases ( len F = 0 or len F >= 1 ) by NAT_1:14;
supposeA4: len F = 0 ; ::_thesis: Sum F = addnat "**" F
hence addnat "**" F = 0 by Def8, A2, BINOP_2:5
.= Sum F by Def8, A3, A4, BINOP_2:1 ;
::_thesis: verum
end;
supposeA5: len F >= 1 ; ::_thesis: Sum F = addnat "**" F
A6: NAT = NAT /\ COMPLEX by MEMBERED:1, XBOOLE_1:28;
now__::_thesis:_for_x,_y_being_set_st_x_in_NAT_&_y_in_NAT_holds_
(_addnat_._(x,y)_=_addcomplex_._(x,y)_&_addnat_._(x,y)_in_NAT_)
let x, y be set ; ::_thesis: ( x in NAT & y in NAT implies ( addnat . (x,y) = addcomplex . (x,y) & addnat . (x,y) in NAT ) )
assume ( x in NAT & y in NAT ) ; ::_thesis: ( addnat . (x,y) = addcomplex . (x,y) & addnat . (x,y) in NAT )
then reconsider X = x, Y = y as Element of NAT ;
addnat . (x,y) = X + Y by BINOP_2:def_23;
hence ( addnat . (x,y) = addcomplex . (x,y) & addnat . (x,y) in NAT ) by BINOP_2:def_3; ::_thesis: verum
end;
hence Sum F = addnat "**" F by Th47, A5, A6, A2; ::_thesis: verum
end;
end;
end;
registration
let F be real-valued XFinSequence;
cluster Sum F -> real ;
coherence
Sum F is real
proof
Sum F = addreal "**" F by Th48;
hence Sum F is real ; ::_thesis: verum
end;
end;
registration
let F be RAT -valued XFinSequence;
cluster Sum F -> rational ;
coherence
Sum F is rational
proof
Sum F = addrat "**" F by Th49;
hence Sum F is rational ; ::_thesis: verum
end;
end;
registration
let F be INT -valued XFinSequence;
cluster Sum F -> integer ;
coherence
Sum F is integer
proof
Sum F = addint "**" F by Th50;
hence Sum F is integer ; ::_thesis: verum
end;
end;
registration
let F be natural-valued XFinSequence;
cluster Sum F -> natural ;
coherence
Sum F is natural
proof
Sum F = addnat "**" F by Th51;
hence Sum F is natural ; ::_thesis: verum
end;
end;
registration
cluster Relation-like natural-valued -> nonnegative-yielding for set ;
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is nonnegative-yielding
proof
let R be Relation; ::_thesis: ( R is natural-valued implies R is nonnegative-yielding )
assume R is natural-valued ; ::_thesis: R is nonnegative-yielding
then for r being real number st r in rng R holds
r >= 0 ;
hence R is nonnegative-yielding by PARTFUN3:def_4; ::_thesis: verum
end;
end;
theorem :: AFINSQ_2:52
for cF being complex-valued XFinSequence st cF = {} holds
Sum cF = 0 ;
theorem :: AFINSQ_2:53
for c being complex number holds Sum <%c%> = c
proof
let c be complex number ; ::_thesis: Sum <%c%> = c
c in COMPLEX by XCMPLX_0:def_2;
hence Sum <%c%> = c by Th37; ::_thesis: verum
end;
theorem :: AFINSQ_2:54
for c1, c2 being complex number holds Sum <%c1,c2%> = c1 + c2
proof
let c1, c2 be complex number ; ::_thesis: Sum <%c1,c2%> = c1 + c2
( c1 in COMPLEX & c2 in COMPLEX ) by XCMPLX_0:def_2;
then addcomplex "**" <%c1,c2%> = addcomplex . (c1,c2) by Th38
.= c1 + c2 by BINOP_2:def_3 ;
hence Sum <%c1,c2%> = c1 + c2 ; ::_thesis: verum
end;
theorem Th55: :: AFINSQ_2:55
for cF1, cF2 being complex-valued XFinSequence holds Sum (cF1 ^ cF2) = (Sum cF1) + (Sum cF2)
proof
let cF1, cF2 be complex-valued XFinSequence; ::_thesis: Sum (cF1 ^ cF2) = (Sum cF1) + (Sum cF2)
A1: ( cF1 is COMPLEX -valued & cF2 is COMPLEX -valued ) by Lm3;
thus Sum (cF1 ^ cF2) = addcomplex . ((Sum cF1),(Sum cF2)) by Th42, A1
.= (Sum cF1) + (Sum cF2) by BINOP_2:def_3 ; ::_thesis: verum
end;
theorem :: AFINSQ_2:56
for n being Nat
for rF being real-valued XFinSequence
for S being Real_Sequence st rF = S | (n + 1) holds
Sum rF = (Partial_Sums S) . n
proof
let n be Nat; ::_thesis: for rF being real-valued XFinSequence
for S being Real_Sequence st rF = S | (n + 1) holds
Sum rF = (Partial_Sums S) . n
let rF be real-valued XFinSequence; ::_thesis: for S being Real_Sequence st rF = S | (n + 1) holds
Sum rF = (Partial_Sums S) . n
let S be Real_Sequence; ::_thesis: ( rF = S | (n + 1) implies Sum rF = (Partial_Sums S) . n )
A1: rF is REAL -valued by Lm4;
n + 1 c= NAT by ORDINAL1:def_2;
then A2: n + 1 c= dom S by FUNCT_2:def_1;
assume A3: rF = S | (n + 1) ; ::_thesis: Sum rF = (Partial_Sums S) . n
then dom rF = (dom S) /\ (n + 1) by RELAT_1:61;
then A4: dom rF = n + 1 by A2, XBOOLE_1:28;
then consider f being Function of NAT,REAL such that
A5: f . 0 = rF . 0 and
A6: for m being Nat st m + 1 < len rF holds
f . (m + 1) = addreal . ((f . m),(rF . (m + 1))) and
A7: addreal "**" rF = f . ((len rF) - 1) by Def8, A1;
defpred S1[ Nat] means ( $1 in dom rF implies f . $1 = (Partial_Sums S) . $1 );
A8: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
assume A10: k + 1 in dom rF ; ::_thesis: f . (k + 1) = (Partial_Sums S) . (k + 1)
then A11: k + 1 < len rF by NAT_1:44;
then A12: k < len rF by NAT_1:13;
A13: k in NAT by ORDINAL1:def_12;
thus f . (k + 1) = addreal . ((f . k),(rF . (k + 1))) by A6, A11
.= (f . k) + (rF . (k + 1)) by BINOP_2:def_9
.= (f . k) + (S . (k + 1)) by A3, A10, FUNCT_1:47
.= (Partial_Sums S) . (k + 1) by A9, A12, A13, NAT_1:44, SERIES_1:def_1 ; ::_thesis: verum
end;
end;
(Partial_Sums S) . 0 = S . 0 by SERIES_1:def_1;
then A14: S1[ 0 ] by A3, A5, FUNCT_1:47;
for m being Nat holds S1[m] from NAT_1:sch_2(A14, A8);
hence (Partial_Sums S) . n = f . n by A4, NAT_1:45
.= Sum rF by Th48, A7, A4 ;
::_thesis: verum
end;
theorem Th57: :: AFINSQ_2:57
for rF1, rF2 being real-valued XFinSequence st len rF1 = len rF2 & ( for i being Nat st i in dom rF1 holds
rF1 . i <= rF2 . i ) holds
Sum rF1 <= Sum rF2
proof
let rF1, rF2 be real-valued XFinSequence; ::_thesis: ( len rF1 = len rF2 & ( for i being Nat st i in dom rF1 holds
rF1 . i <= rF2 . i ) implies Sum rF1 <= Sum rF2 )
set d = rF1;
set e = rF2;
assume that
A1: len rF1 = len rF2 and
A2: for i being Nat st i in dom rF1 holds
rF1 . i <= rF2 . i ; ::_thesis: Sum rF1 <= Sum rF2
reconsider d = rF1, e = rF2 as XFinSequence of REAL by Lm4;
A3: ( Sum d = addreal "**" d & Sum e = addreal "**" e ) by Th48;
percases ( len d >= 1 or len d = 0 ) by NAT_1:14;
supposeA4: len d >= 1 ; ::_thesis: Sum rF1 <= Sum rF2
consider f being Function of NAT,REAL such that
A5: f . 0 = d . 0 and
A6: for n being Nat st n + 1 < len d holds
f . (n + 1) = addreal . ((f . n),(d . (n + 1))) and
A7: Sum d = f . ((len d) - 1) by A4, Def8, A3;
consider g being Function of NAT,REAL such that
A8: g . 0 = e . 0 and
A9: for n being Nat st n + 1 < len e holds
g . (n + 1) = addreal . ((g . n),(e . (n + 1))) and
A10: Sum e = g . ((len e) - 1) by A4, A1, Def8, A3;
defpred S1[ Nat] means ( $1 in dom d implies f . $1 <= g . $1 );
A11: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_
S1[i_+_1]
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A12: S1[i] ; ::_thesis: S1[i + 1]
thus S1[i + 1] ::_thesis: verum
proof
assume A13: i + 1 in dom d ; ::_thesis: f . (i + 1) <= g . (i + 1)
then A14: i + 1 < len d by NAT_1:44;
then A15: i < len d by NAT_1:13;
A16: d . (i + 1) <= e . (i + 1) by A2, A13;
A17: f . (i + 1) = addreal . ((f . i),(d . (i + 1))) by A6, A14
.= (f . i) + (d . (i + 1)) by BINOP_2:def_9 ;
g . (i + 1) = addreal . ((g . i),(e . (i + 1))) by A1, A9, A14
.= (g . i) + (e . (i + 1)) by BINOP_2:def_9 ;
hence f . (i + 1) <= g . (i + 1) by A12, A15, A17, A16, NAT_1:44, XREAL_1:7; ::_thesis: verum
end;
end;
reconsider ld = (len d) - 1 as Element of NAT by A4, NAT_1:21;
(len d) - 1 < (len d) - 0 by XREAL_1:10;
then A18: ld in len d by NAT_1:44;
A19: S1[ 0 ] by A2, A5, A8;
for i being Nat holds S1[i] from NAT_1:sch_2(A19, A11);
hence Sum rF1 <= Sum rF2 by A1, A7, A10, A18; ::_thesis: verum
end;
suppose len d = 0 ; ::_thesis: Sum rF1 <= Sum rF2
then ( Sum d = the_unity_wrt addreal & Sum e = the_unity_wrt addreal ) by Def8, A3, A1;
hence Sum rF1 <= Sum rF2 ; ::_thesis: verum
end;
end;
end;
theorem Th58: :: AFINSQ_2:58
for n being Nat
for c being complex number holds Sum (n --> c) = n * c
proof
let n be Nat; ::_thesis: for c being complex number holds Sum (n --> c) = n * c
let c be complex number ; ::_thesis: Sum (n --> c) = n * c
set Fn = n --> c;
reconsider Fn = n --> c as XFinSequence of COMPLEX by Lm3;
A1: dom Fn = n by FUNCOP_1:13;
now__::_thesis:_Sum_(n_-->_c)_=_n_*_c
percases ( dom Fn = 0 or dom Fn > 0 ) ;
suppose dom Fn = 0 ; ::_thesis: Sum (n --> c) = n * c
hence Sum (n --> c) = n * c by A1; ::_thesis: verum
end;
supposeA2: dom Fn > 0 ; ::_thesis: Sum (n --> c) = n * c
then consider f being Function of NAT,COMPLEX such that
A3: f . 0 = Fn . 0 and
A4: for k being Nat st k + 1 < len Fn holds
f . (k + 1) = addcomplex . ((f . k),(Fn . (k + 1))) and
A5: Sum Fn = f . ((len Fn) - 1) by Def8;
defpred S1[ Nat] means ( $1 < len Fn implies f . $1 = ($1 + 1) * c );
A6: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A7: S1[m] ; ::_thesis: S1[m + 1]
assume A8: m + 1 < len Fn ; ::_thesis: f . (m + 1) = ((m + 1) + 1) * c
then f . (m + 1) = addcomplex . ((f . m),(Fn . (m + 1))) by A4;
then A9: f . (m + 1) = (f . m) + (Fn . (m + 1)) by BINOP_2:def_3;
m + 1 in len Fn by A8, NAT_1:44;
then Fn . (m + 1) = c by A1, FUNCOP_1:7;
hence f . (m + 1) = ((m + 1) + 1) * c by A7, A8, A9, NAT_1:13; ::_thesis: verum
end;
reconsider lenFn1 = (len Fn) - 1 as Element of NAT by A2, NAT_1:20;
A10: lenFn1 < lenFn1 + 1 by NAT_1:13;
A11: S1[ 0 ]
proof
assume 0 < len Fn ; ::_thesis: f . 0 = (0 + 1) * c
then 0 in dom Fn by NAT_1:44;
hence f . 0 = (0 + 1) * c by A3, A1, FUNCOP_1:7; ::_thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch_2(A11, A6);
hence Sum (n --> c) = n * c by A5, A10, A1; ::_thesis: verum
end;
end;
end;
hence Sum (n --> c) = n * c ; ::_thesis: verum
end;
theorem :: AFINSQ_2:59
for rF being real-valued XFinSequence
for r being real number st ( for n being Nat st n in dom rF holds
rF . n <= r ) holds
Sum rF <= (len rF) * r
proof
let rF be real-valued XFinSequence; ::_thesis: for r being real number st ( for n being Nat st n in dom rF holds
rF . n <= r ) holds
Sum rF <= (len rF) * r
let r be real number ; ::_thesis: ( ( for n being Nat st n in dom rF holds
rF . n <= r ) implies Sum rF <= (len rF) * r )
set L = (len rF) --> r;
assume A1: for n being Nat st n in dom rF holds
rF . n <= r ; ::_thesis: Sum rF <= (len rF) * r
A2: len ((len rF) --> r) = len rF by FUNCOP_1:13;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_rF_holds_
rF_._n_<=_((len_rF)_-->_r)_._n
let n be Nat; ::_thesis: ( n in dom rF implies rF . n <= ((len rF) --> r) . n )
assume n in dom rF ; ::_thesis: rF . n <= ((len rF) --> r) . n
then ( rF . n <= r & ((len rF) --> r) . n = r ) by A1, FUNCOP_1:7;
hence rF . n <= ((len rF) --> r) . n ; ::_thesis: verum
end;
then Sum rF <= Sum ((len rF) --> r) by Th57, A2;
hence Sum rF <= (len rF) * r by Th58; ::_thesis: verum
end;
theorem :: AFINSQ_2:60
for rF being real-valued XFinSequence
for r being real number st ( for n being Nat st n in dom rF holds
rF . n >= r ) holds
Sum rF >= (len rF) * r
proof
let rF be real-valued XFinSequence; ::_thesis: for r being real number st ( for n being Nat st n in dom rF holds
rF . n >= r ) holds
Sum rF >= (len rF) * r
let r be real number ; ::_thesis: ( ( for n being Nat st n in dom rF holds
rF . n >= r ) implies Sum rF >= (len rF) * r )
set L = (len rF) --> r;
assume A1: for n being Nat st n in dom rF holds
rF . n >= r ; ::_thesis: Sum rF >= (len rF) * r
A2: len ((len rF) --> r) = len rF by FUNCOP_1:13;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_rF_holds_
rF_._n_>=_((len_rF)_-->_r)_._n
let n be Nat; ::_thesis: ( n in dom rF implies rF . n >= ((len rF) --> r) . n )
assume n in dom rF ; ::_thesis: rF . n >= ((len rF) --> r) . n
then ( rF . n >= r & ((len rF) --> r) . n = r ) by A1, FUNCOP_1:7;
hence rF . n >= ((len rF) --> r) . n ; ::_thesis: verum
end;
then Sum rF >= Sum ((len rF) --> r) by Th57, A2;
hence Sum rF >= (len rF) * r by Th58; ::_thesis: verum
end;
theorem Th61: :: AFINSQ_2:61
for rF being real-valued XFinSequence
for r being real number st rF is nonnegative-yielding & len rF > 0 & ex x being set st
( x in dom rF & rF . x = r ) holds
Sum rF >= r
proof
let rF be real-valued XFinSequence; ::_thesis: for r being real number st rF is nonnegative-yielding & len rF > 0 & ex x being set st
( x in dom rF & rF . x = r ) holds
Sum rF >= r
let r be real number ; ::_thesis: ( rF is nonnegative-yielding & len rF > 0 & ex x being set st
( x in dom rF & rF . x = r ) implies Sum rF >= r )
assume that
A1: rF is nonnegative-yielding and
A2: len rF > 0 and
A3: ex x being set st
( x in dom rF & rF . x = r ) ; ::_thesis: Sum rF >= r
consider x being set such that
A4: x in dom rF and
A5: rF . x = r by A3;
reconsider lenrF1 = (len rF) - 1 as Element of NAT by A2, NAT_1:20;
A6: dom rF = lenrF1 + 1 ;
reconsider x = x as Element of NAT by A4;
A7: lenrF1 < lenrF1 + 1 by NAT_1:13;
A8: x < dom rF by A4, NAT_1:44;
then A9: x <= lenrF1 by A6, NAT_1:13;
rF is REAL -valued by Lm4;
then consider f being Function of NAT,REAL such that
A10: f . 0 = rF . 0 and
A11: for n being Nat st n + 1 < len rF holds
f . (n + 1) = addreal . ((f . n),(rF . (n + 1))) and
A12: addreal "**" rF = f . ((len rF) - 1) by Def8, A2;
defpred S1[ Nat] means ( $1 < x implies f . $1 >= 0 );
0 in len rF by A2, NAT_1:44;
then rF . 0 in rng rF by FUNCT_1:def_3;
then A13: S1[ 0 ] by A1, A10, PARTFUN3:def_4;
A14: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A15: S1[n] ; ::_thesis: S1[n + 1]
assume A16: n + 1 < x ; ::_thesis: f . (n + 1) >= 0
then ( n < x & n + 1 < len rF ) by A8, NAT_1:13, XXREAL_0:2;
then A17: ( f . (n + 1) = addreal . ((f . n),(rF . (n + 1))) & f . n >= 0 & n + 1 in dom rF ) by A11, A15, NAT_1:44;
then rF . (n + 1) in rng rF by FUNCT_1:def_3;
then rF . (n + 1) >= 0 by A1, PARTFUN3:def_4;
then (f . n) + (rF . (n + 1)) >= 0 + 0 by A16, A15, NAT_1:13;
hence f . (n + 1) >= 0 by A17, BINOP_2:def_9; ::_thesis: verum
end;
A18: for n being Nat holds S1[n] from NAT_1:sch_2(A13, A14);
defpred S2[ Nat] means ( x <= $1 & $1 < len rF implies f . $1 >= r );
now__::_thesis:_(_x_<=_x_&_x_<_len_rF_implies_f_._x_>=_r_)
percases ( x = 0 or x > 0 ) ;
supposeA19: x = 0 ; ::_thesis: ( x <= x & x < len rF implies f . x >= r )
assume that
x <= x and
x < len rF ; ::_thesis: f . x >= r
thus f . x >= r by A5, A10, A19; ::_thesis: verum
end;
suppose x > 0 ; ::_thesis: ( x <= x & x < len rF implies f . x >= r )
then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
assume that
x <= x and
A20: x < len rF ; ::_thesis: f . x >= r
A21: x1 < x1 + 1 by NAT_1:13;
x1 + 1 < len rF by A20;
then f . x = addreal . ((f . x1),(rF . x)) by A11;
then ( f . x = (f . x1) + (rF . x) & f . x1 >= 0 ) by A21, A18, BINOP_2:def_9;
then f . x >= r + 0 by A5, XREAL_1:7;
hence f . x >= r ; ::_thesis: verum
end;
end;
end;
then A22: S2[x] ;
A23: for m being Nat st m >= x & S2[m] holds
S2[m + 1]
proof
let m be Nat; ::_thesis: ( m >= x & S2[m] implies S2[m + 1] )
assume that
A24: m >= x and
A25: S2[m] ; ::_thesis: S2[m + 1]
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
assume that
x <= m + 1 and
A26: m + 1 < len rF ; ::_thesis: f . (m + 1) >= r
m + 1 in dom rF by A26, NAT_1:44;
then A27: rF . (m + 1) in rng rF by FUNCT_1:def_3;
f . (m1 + 1) = addreal . ((f . m1),(rF . (m1 + 1))) by A11, A26;
then ( f . (m1 + 1) = (f . m1) + (rF . (m1 + 1)) & rF . (m1 + 1) >= 0 ) by A27, A1, BINOP_2:def_9, PARTFUN3:def_4;
then f . (m + 1) >= r + 0 by A24, A25, A26, NAT_1:13, XREAL_1:7;
hence f . (m + 1) >= r ; ::_thesis: verum
end;
for m being Nat st m >= x holds
S2[m] from NAT_1:sch_8(A22, A23);
then addreal "**" rF >= r by A12, A9, A7;
hence Sum rF >= r by Th48; ::_thesis: verum
end;
theorem Th62: :: AFINSQ_2:62
for rF being real-valued XFinSequence st rF is nonnegative-yielding holds
( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) )
proof
let rF be real-valued XFinSequence; ::_thesis: ( rF is nonnegative-yielding implies ( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) ) )
assume A1: rF is nonnegative-yielding ; ::_thesis: ( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) )
hereby ::_thesis: ( ( len rF = 0 or rF = (len rF) --> 0 ) implies Sum rF = 0 )
assume A2: Sum rF = 0 ; ::_thesis: ( len rF <> 0 implies not rF <> (len rF) --> 0 )
assume len rF <> 0 ; ::_thesis: not rF <> (len rF) --> 0
set L = (len rF) --> 0;
assume rF <> (len rF) --> 0 ; ::_thesis: contradiction
then consider k being Nat such that
A3: ( k in dom ((len rF) --> 0) & ((len rF) --> 0) . k <> rF . k ) by AFINSQ_1:8, FUNCOP_1:13;
rF . k in rng rF by A3, FUNCT_1:def_3;
then ( ((len rF) --> 0) . k = 0 & rF . k >= 0 ) by A3, A1, FUNCOP_1:7, PARTFUN3:def_4;
hence contradiction by A2, Th61, A1, A3; ::_thesis: verum
end;
A4: rF is COMPLEX -valued by Lm3;
assume ( len rF = 0 or rF = (len rF) --> 0 ) ; ::_thesis: Sum rF = 0
then ( Sum rF = 0 or Sum rF = (len rF) * 0 ) by A4, Th58, Def8, BINOP_2:1;
hence Sum rF = 0 ; ::_thesis: verum
end;
theorem Th63: :: AFINSQ_2:63
for n being Nat
for cF being complex-valued XFinSequence
for c being complex number holds c (#) (cF | n) = (c (#) cF) | n
proof
let n be Nat; ::_thesis: for cF being complex-valued XFinSequence
for c being complex number holds c (#) (cF | n) = (c (#) cF) | n
let cF be complex-valued XFinSequence; ::_thesis: for c being complex number holds c (#) (cF | n) = (c (#) cF) | n
let c be complex number ; ::_thesis: c (#) (cF | n) = (c (#) cF) | n
set ccF = c (#) cF;
set cFn = cF | n;
A1: ( len (c (#) cF) = len cF & len (c (#) (cF | n)) = len (cF | n) ) by VALUED_1:def_5;
percases ( n <= len cF or n > len cF ) ;
supposeA2: n <= len cF ; ::_thesis: c (#) (cF | n) = (c (#) cF) | n
then A3: ( len (cF | n) = n & len ((c (#) cF) | n) = n ) by A1, AFINSQ_1:54;
now__::_thesis:_for_i_being_Nat_st_i_<_len_(c_(#)_(cF_|_n))_holds_
(c_(#)_(cF_|_n))_._i_=_((c_(#)_cF)_|_n)_._i
let i be Nat; ::_thesis: ( i < len (c (#) (cF | n)) implies (c (#) (cF | n)) . i = ((c (#) cF) | n) . i )
assume i < len (c (#) (cF | n)) ; ::_thesis: (c (#) (cF | n)) . i = ((c (#) cF) | n) . i
then A4: i in dom (c (#) (cF | n)) by NAT_1:44;
thus (c (#) (cF | n)) . i = c * ((cF | n) . i) by VALUED_1:6
.= c * (cF . i) by A4, A2, AFINSQ_1:53
.= (c (#) cF) . i by VALUED_1:6
.= ((c (#) cF) | n) . i by A4, A1, A2, AFINSQ_1:53 ; ::_thesis: verum
end;
hence c (#) (cF | n) = (c (#) cF) | n by A1, A3, AFINSQ_1:9; ::_thesis: verum
end;
suppose n > len cF ; ::_thesis: c (#) (cF | n) = (c (#) cF) | n
then ( cF | n = cF & (c (#) cF) | n = c (#) cF ) by A1, AFINSQ_1:52;
hence c (#) (cF | n) = (c (#) cF) | n ; ::_thesis: verum
end;
end;
end;
theorem :: AFINSQ_2:64
for cF being complex-valued XFinSequence
for c being complex number holds c * (Sum cF) = Sum (c (#) cF)
proof
let cF be complex-valued XFinSequence; ::_thesis: for c being complex number holds c * (Sum cF) = Sum (c (#) cF)
let c be complex number ; ::_thesis: c * (Sum cF) = Sum (c (#) cF)
defpred S1[ Nat] means for cF being complex-valued XFinSequence st dom cF = $1 holds
c * (Sum cF) = Sum (c (#) cF);
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
A3: k < k + 1 by NAT_1:13;
let cF be complex-valued XFinSequence; ::_thesis: ( dom cF = k + 1 implies c * (Sum cF) = Sum (c (#) cF) )
assume A4: dom cF = k + 1 ; ::_thesis: c * (Sum cF) = Sum (c (#) cF)
set cF1 = c (#) cF;
A5: dom cF = dom (c (#) cF) by VALUED_1:def_5;
reconsider cF = cF, cF1 = c (#) cF as XFinSequence of COMPLEX by Lm3;
A6: cF | (k + 1) = cF by A4, RELAT_1:69;
len cF = k + 1 by A4;
then A7: len (cF | k) = k by A3, AFINSQ_1:11;
k < k + 1 by NAT_1:13;
then A8: k in dom cF by A4, NAT_1:44;
then addcomplex . ((addcomplex "**" (cF | k)),(cF . k)) = addcomplex "**" (cF | (k + 1)) by Th43;
then A9: Sum cF = (Sum (cF | k)) + (cF . k) by A6, BINOP_2:def_3;
A10: c * (Sum (cF | k)) = Sum (c (#) (cF | k)) by A2, A7
.= Sum (cF1 | k) by Th63 ;
A11: c * (cF . k) = cF1 . k by VALUED_1:6;
A12: cF1 | (k + 1) = cF1 by A4, A5, RELAT_1:69;
addcomplex . ((addcomplex "**" (cF1 | k)),(cF1 . k)) = addcomplex "**" (cF1 | (k + 1)) by A5, A8, Th43;
then Sum cF1 = (Sum (cF1 | k)) + (cF1 . k) by A12, BINOP_2:def_3;
hence c * (Sum cF) = Sum (c (#) cF) by A9, A11, A10; ::_thesis: verum
end;
A13: S1[ 0 ]
proof
let cF be complex-valued XFinSequence; ::_thesis: ( dom cF = 0 implies c * (Sum cF) = Sum (c (#) cF) )
assume A14: dom cF = 0 ; ::_thesis: c * (Sum cF) = Sum (c (#) cF)
set cF1 = c (#) cF;
reconsider cF = cF, cF1 = c (#) cF as XFinSequence of COMPLEX by Lm3;
len cF = 0 by A14;
then A15: addcomplex "**" cF = 0 by Def8, BINOP_2:1;
len cF1 = 0 by A14, VALUED_1:def_5;
hence c * (Sum cF) = Sum (c (#) cF) by A15, Def8, BINOP_2:1; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A13, A1);
then S1[ len cF] ;
hence c * (Sum cF) = Sum (c (#) cF) ; ::_thesis: verum
end;
theorem Th65: :: AFINSQ_2:65
for n being Nat
for cF being complex-valued XFinSequence st n in dom cF holds
(Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1))
proof
let n be Nat; ::_thesis: for cF being complex-valued XFinSequence st n in dom cF holds
(Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1))
let cF be complex-valued XFinSequence; ::_thesis: ( n in dom cF implies (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1)) )
assume A1: n in dom cF ; ::_thesis: (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1))
reconsider cF = cF as XFinSequence of COMPLEX by Lm3;
addcomplex . ((addcomplex "**" (cF | n)),(cF . n)) = addcomplex "**" (cF | (n + 1)) by Th43, A1;
hence (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1)) by BINOP_2:def_3; ::_thesis: verum
end;
theorem Th66: :: AFINSQ_2:66
for y, x being set
for f being Function st f . y = x & y in dom f holds
{y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}
proof
let y, x be set ; ::_thesis: for f being Function st f . y = x & y in dom f holds
{y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}
let f be Function; ::_thesis: ( f . y = x & y in dom f implies {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x} )
assume that
A1: f . y = x and
A2: y in dom f ; ::_thesis: {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}
set d = (dom f) \ {y};
A3: (f | ((dom f) \ {y})) " {x} c= f " {x}
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in (f | ((dom f) \ {y})) " {x} or x1 in f " {x} )
assume A4: x1 in (f | ((dom f) \ {y})) " {x} ; ::_thesis: x1 in f " {x}
A5: (f | ((dom f) \ {y})) . x1 in {x} by A4, FUNCT_1:def_7;
A6: x1 in dom (f | ((dom f) \ {y})) by A4, FUNCT_1:def_7;
then ( dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) & f . x1 = (f | ((dom f) \ {y})) . x1 ) by FUNCT_1:47, RELAT_1:61;
hence x1 in f " {x} by A6, A5, FUNCT_1:def_7; ::_thesis: verum
end;
A7: f " {x} c= {y} \/ ((f | ((dom f) \ {y})) " {x})
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in f " {x} or x1 in {y} \/ ((f | ((dom f) \ {y})) " {x}) )
assume A8: x1 in f " {x} ; ::_thesis: x1 in {y} \/ ((f | ((dom f) \ {y})) " {x})
( ( x1 in dom f & not x1 in {y} ) or x1 = y ) by A8, FUNCT_1:def_7, TARSKI:def_1;
then ( ( x1 in dom f & x1 in (dom f) \ {y} & dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) ) or x1 = y ) by RELAT_1:61, XBOOLE_0:def_5;
then ( x1 in dom (f | ((dom f) \ {y})) or x1 = y ) by XBOOLE_0:def_4;
then ( ( x1 in dom (f | ((dom f) \ {y})) & f . x1 = (f | ((dom f) \ {y})) . x1 & f . x1 in {x} ) or x1 in {y} ) by A8, FUNCT_1:47, FUNCT_1:def_7, TARSKI:def_1;
then ( x1 in (f | ((dom f) \ {y})) " {x} or x1 in {y} ) by FUNCT_1:def_7;
hence x1 in {y} \/ ((f | ((dom f) \ {y})) " {x}) by XBOOLE_0:def_3; ::_thesis: verum
end;
{y} c= f " {x}
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {y} or z in f " {x} )
assume z in {y} ; ::_thesis: z in f " {x}
then A9: z = y by TARSKI:def_1;
f . y in {x} by A1, TARSKI:def_1;
hence z in f " {x} by A2, A9, FUNCT_1:def_7; ::_thesis: verum
end;
then {y} \/ ((f | ((dom f) \ {y})) " {x}) c= f " {x} by A3, XBOOLE_1:8;
hence {y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x} by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th67: :: AFINSQ_2:67
for y, x being set
for f being Function st f . y <> x holds
(f | ((dom f) \ {y})) " {x} = f " {x}
proof
let y, x be set ; ::_thesis: for f being Function st f . y <> x holds
(f | ((dom f) \ {y})) " {x} = f " {x}
let f be Function; ::_thesis: ( f . y <> x implies (f | ((dom f) \ {y})) " {x} = f " {x} )
set d = (dom f) \ {y};
assume A1: f . y <> x ; ::_thesis: (f | ((dom f) \ {y})) " {x} = f " {x}
A2: f " {x} c= (f | ((dom f) \ {y})) " {x}
proof
A3: dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) by RELAT_1:61;
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in f " {x} or x1 in (f | ((dom f) \ {y})) " {x} )
assume A4: x1 in f " {x} ; ::_thesis: x1 in (f | ((dom f) \ {y})) " {x}
A5: f . x1 in {x} by A4, FUNCT_1:def_7;
f . x1 in {x} by A4, FUNCT_1:def_7;
then f . x1 = x by TARSKI:def_1;
then A6: not x1 in {y} by A1, TARSKI:def_1;
x1 in dom f by A4, FUNCT_1:def_7;
then x1 in (dom f) \ {y} by A6, XBOOLE_0:def_5;
then A7: x1 in dom (f | ((dom f) \ {y})) by A3, XBOOLE_0:def_4;
then f . x1 = (f | ((dom f) \ {y})) . x1 by FUNCT_1:47;
hence x1 in (f | ((dom f) \ {y})) " {x} by A7, A5, FUNCT_1:def_7; ::_thesis: verum
end;
(f | ((dom f) \ {y})) " {x} c= f " {x}
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in (f | ((dom f) \ {y})) " {x} or x1 in f " {x} )
assume A8: x1 in (f | ((dom f) \ {y})) " {x} ; ::_thesis: x1 in f " {x}
A9: (f | ((dom f) \ {y})) . x1 in {x} by A8, FUNCT_1:def_7;
A10: x1 in dom (f | ((dom f) \ {y})) by A8, FUNCT_1:def_7;
then ( dom (f | ((dom f) \ {y})) = (dom f) /\ ((dom f) \ {y}) & f . x1 = (f | ((dom f) \ {y})) . x1 ) by FUNCT_1:47, RELAT_1:61;
hence x1 in f " {x} by A10, A9, FUNCT_1:def_7; ::_thesis: verum
end;
hence (f | ((dom f) \ {y})) " {x} = f " {x} by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: AFINSQ_2:68
for cF being complex-valued XFinSequence
for c being complex number st rng cF c= {0,c} holds
Sum cF = c * (card (cF " {c}))
proof
let cF be complex-valued XFinSequence; ::_thesis: for c being complex number st rng cF c= {0,c} holds
Sum cF = c * (card (cF " {c}))
let c be complex number ; ::_thesis: ( rng cF c= {0,c} implies Sum cF = c * (card (cF " {c})) )
defpred S1[ Nat] means for cF being complex-valued XFinSequence
for c being complex number st dom cF = $1 & rng cF c= {0,c} holds
Sum cF = c * (card (cF " {c}));
assume A1: rng cF c= {0,c} ; ::_thesis: Sum cF = c * (card (cF " {c}))
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
let F be complex-valued XFinSequence; ::_thesis: for c being complex number st dom F = k + 1 & rng F c= {0,c} holds
Sum F = c * (card (F " {c}))
let c be complex number ; ::_thesis: ( dom F = k + 1 & rng F c= {0,c} implies Sum F = c * (card (F " {c})) )
assume that
A4: dom F = k + 1 and
A5: rng F c= {0,c} ; ::_thesis: Sum F = c * (card (F " {c}))
percases ( c <> 0 or c = 0 ) ;
supposeA6: c <> 0 ; ::_thesis: Sum F = c * (card (F " {c}))
( not k in k & k \/ {k} = k + 1 ) by AFINSQ_1:2;
then A7: (dom F) \ {k} = k by A4, ZFMISC_1:117;
k < k + 1 by NAT_1:13;
then k in dom F by A4, NAT_1:44;
then A8: F . k in rng F by FUNCT_1:def_3;
percases ( F . k = 0 or F . k = c ) by A5, A8, TARSKI:def_2;
supposeA9: F . k = 0 ; ::_thesis: Sum F = c * (card (F " {c}))
A10: F | (k + 1) = F by A4, RELAT_1:69;
A11: k < k + 1 by NAT_1:13;
then k in dom F by A4, NAT_1:44;
then A12: (Sum (F | k)) + 0 = Sum F by A9, A10, Th65;
dom F = len F ;
then A13: len (F | k) = k by A4, A11, AFINSQ_1:54;
( rng (F | k) c= rng F & (F | k) " {c} = F " {c} ) by A6, A7, A9, Th67;
hence Sum F = c * (card (F " {c})) by A3, A5, A13, A12, XBOOLE_1:1; ::_thesis: verum
end;
supposeA14: F . k = c ; ::_thesis: Sum F = c * (card (F " {c}))
set Fk = (F | k) " {c};
not k in k ;
then not k in dom (F | k) ;
then A15: not k in (F | k) " {c} by FUNCT_1:def_7;
A16: k < k + 1 by NAT_1:13;
then A17: k in dom F by A4, NAT_1:44;
dom F = len F ;
then ( rng (F | k) c= rng F & len (F | k) = k ) by A4, A16, AFINSQ_1:54;
then A18: Sum (F | k) = c * (card ((F | k) " {c})) by A3, A5, XBOOLE_1:1;
F | (k + 1) = F by A4, RELAT_1:69;
then A19: (Sum (F | k)) + c = Sum F by A14, A17, Th65;
{k} \/ ((F | k) " {c}) = F " {c} by A7, A14, A17, Th66;
then (card ((F | k) " {c})) + 1 = card (F " {c}) by A15, CARD_2:41;
hence Sum F = c * (card (F " {c})) by A18, A19; ::_thesis: verum
end;
end;
end;
supposeA20: c = 0 ; ::_thesis: Sum F = c * (card (F " {c}))
for x being set st x in dom F holds
F . x = 0
proof
let x be set ; ::_thesis: ( x in dom F implies F . x = 0 )
assume x in dom F ; ::_thesis: F . x = 0
then F . x in rng F by FUNCT_1:def_3;
hence F . x = 0 by A5, A20, TARSKI:def_2; ::_thesis: verum
end;
then F = (dom F) --> 0 by FUNCOP_1:11;
then Sum F = (len F) * 0 by Th62;
hence Sum F = c * (card (F " {c})) by A20; ::_thesis: verum
end;
end;
end;
A21: S1[ 0 ]
proof
let F be complex-valued XFinSequence; ::_thesis: for c being complex number st dom F = 0 & rng F c= {0,c} holds
Sum F = c * (card (F " {c}))
let c be complex number ; ::_thesis: ( dom F = 0 & rng F c= {0,c} implies Sum F = c * (card (F " {c})) )
assume that
A22: dom F = 0 and
rng F c= {0,c} ; ::_thesis: Sum F = c * (card (F " {c}))
( F " {c} c= 0 & F = {} ) by A22, RELAT_1:132;
then ( card (F " {c}) = 0 & Sum F = 0 ) ;
hence Sum F = c * (card (F " {c})) ; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A21, A2);
then S1[ len cF] ;
hence Sum cF = c * (card (cF " {c})) by A1; ::_thesis: verum
end;
theorem :: AFINSQ_2:69
for cF being complex-valued XFinSequence holds Sum cF = Sum (Rev cF)
proof
let cF be complex-valued XFinSequence; ::_thesis: Sum cF = Sum (Rev cF)
cF is COMPLEX -valued by Lm3;
then reconsider Fr2 = cF, Fr1 = Rev cF as XFinSequence of COMPLEX ;
A1: len Fr1 = len Fr2 by Def1;
defpred S1[ set , set ] means for i being Nat st i = $1 holds
$2 = (len Fr1) - (1 + i);
A2: card (len Fr1) = card (len Fr1) ;
A3: for x being set st x in len Fr1 holds
ex y being set st
( y in len Fr1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in len Fr1 implies ex y being set st
( y in len Fr1 & S1[x,y] ) )
assume A4: x in len Fr1 ; ::_thesis: ex y being set st
( y in len Fr1 & S1[x,y] )
reconsider k = x as Element of NAT by Th1, A4;
k < len Fr1 by A4, NAT_1:44;
then k + 1 <= len Fr1 by NAT_1:13;
then A5: (len Fr1) -' (1 + k) = (len Fr1) - (1 + k) by XREAL_1:233;
take (len Fr1) -' (1 + k) ; ::_thesis: ( (len Fr1) -' (1 + k) in len Fr1 & S1[x,(len Fr1) -' (1 + k)] )
(len Fr1) + 0 < (len Fr1) + (1 + k) by XREAL_1:8;
then (len Fr1) - (1 + k) < ((len Fr1) + (1 + k)) - (1 + k) by XREAL_1:9;
hence ( (len Fr1) -' (1 + k) in len Fr1 & S1[x,(len Fr1) -' (1 + k)] ) by A5, NAT_1:44; ::_thesis: verum
end;
consider P being Function of (len Fr1),(len Fr1) such that
A6: for x being set st x in len Fr1 holds
S1[x,P . x] from FUNCT_2:sch_1(A3);
A7: for x1, x2 being set st x1 in len Fr1 & x2 in len Fr1 & P . x1 = P . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in len Fr1 & x2 in len Fr1 & P . x1 = P . x2 implies x1 = x2 )
assume that
A8: x1 in len Fr1 and
A9: x2 in len Fr1 and
A10: P . x1 = P . x2 ; ::_thesis: x1 = x2
reconsider i = x1, j = x2 as Element of NAT by A8, A9, Th1;
A11: P . x2 = (len Fr1) - (1 + j) by A6, A9;
P . x1 = (len Fr1) - (1 + i) by A6, A8;
hence x1 = x2 by A10, A11; ::_thesis: verum
end;
then A12: P is one-to-one by FUNCT_2:56;
P is one-to-one by A7, FUNCT_2:56;
then P is onto by A2, Lm2;
then reconsider P = P as Permutation of (dom Fr1) by A12;
A13: now__::_thesis:_for_x_being_set_st_x_in_dom_Fr1_holds_
Fr1_._x_=_Fr2_._(P_._x)
let x be set ; ::_thesis: ( x in dom Fr1 implies Fr1 . x = Fr2 . (P . x) )
assume A14: x in dom Fr1 ; ::_thesis: Fr1 . x = Fr2 . (P . x)
reconsider k = x as Element of NAT by A14;
P . k = (len Fr1) - (1 + k) by A6, A14;
hence Fr1 . x = Fr2 . (P . x) by A1, Def1, A14; ::_thesis: verum
end;
A15: now__::_thesis:_for_x_being_set_st_x_in_dom_Fr1_holds_
(_x_in_dom_P_&_P_._x_in_dom_Fr2_)
let x be set ; ::_thesis: ( x in dom Fr1 implies ( x in dom P & P . x in dom Fr2 ) )
assume A16: x in dom Fr1 ; ::_thesis: ( x in dom P & P . x in dom Fr2 )
x in dom P by A16, FUNCT_2:52;
then P . x in rng P by FUNCT_1:3;
hence ( x in dom P & P . x in dom Fr2 ) by A1, A16, FUNCT_2:52; ::_thesis: verum
end;
for x being set st x in dom P & P . x in dom Fr2 holds
x in dom Fr1 ;
then Fr1 = Fr2 * P by A15, A13, FUNCT_1:10;
hence Sum cF = Sum (Rev cF) by A1, Th45; ::_thesis: verum
end;
theorem Th70: :: AFINSQ_2:70
for f being Function
for p, q, fp, fq being XFinSequence st rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q holds
fp ^ fq = f * (p ^ q)
proof
let f be Function; ::_thesis: for p, q, fp, fq being XFinSequence st rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q holds
fp ^ fq = f * (p ^ q)
let p, q, fp, fq be XFinSequence; ::_thesis: ( rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q implies fp ^ fq = f * (p ^ q) )
assume A1: ( rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q ) ; ::_thesis: fp ^ fq = f * (p ^ q)
set pq = p ^ q;
A2: rng (p ^ q) = (rng p) \/ (rng q) by AFINSQ_1:26;
then A3: dom (f * (p ^ q)) = dom (p ^ q) by A1, RELAT_1:27, XBOOLE_1:8;
reconsider fpq = f * (p ^ q) as XFinSequence by A2, A1, AFINSQ_1:10, XBOOLE_1:8;
A4: ( dom fp = dom p & dom fq = dom q ) by A1, RELAT_1:27;
A5: ( dom (p ^ q) = (len p) + (len q) & dom (fp ^ fq) = (len fp) + (len fq) ) by AFINSQ_1:def_3;
A6: len fpq = len (fp ^ fq) by A2, A1, A4, A5, RELAT_1:27, XBOOLE_1:8;
for k being Nat st k < len fpq holds
(fp ^ fq) . k = fpq . k
proof
let k be Nat; ::_thesis: ( k < len fpq implies (fp ^ fq) . k = fpq . k )
assume A7: k < len fpq ; ::_thesis: (fp ^ fq) . k = fpq . k
then A8: k in dom fpq by NAT_1:44;
percases ( k < len p or k >= len p ) ;
suppose k < len p ; ::_thesis: (fp ^ fq) . k = fpq . k
then k in dom p by NAT_1:44;
then ( (p ^ q) . k = p . k & fp . k = f . (p . k) & (fp ^ fq) . k = fp . k ) by A1, A4, AFINSQ_1:def_3, FUNCT_1:13;
hence (fp ^ fq) . k = fpq . k by A8, FUNCT_1:12; ::_thesis: verum
end;
supposeA9: k >= len p ; ::_thesis: (fp ^ fq) . k = fpq . k
then reconsider kp = k - (len p) as Element of NAT by NAT_1:21;
(len p) + kp < (len p) + (len q) by A5, A2, A1, A7, RELAT_1:27, XBOOLE_1:8;
then kp < len q by XREAL_1:7;
then kp in dom q by NAT_1:44;
then ( (p ^ q) . k = q . kp & (fp ^ fq) . k = fq . kp & fq . kp = f . (q . kp) ) by A7, A1, A3, A4, A5, A9, AFINSQ_1:18, FUNCT_1:13;
hence (fp ^ fq) . k = fpq . k by A8, FUNCT_1:12; ::_thesis: verum
end;
end;
end;
hence fp ^ fq = f * (p ^ q) by A6, AFINSQ_1:9; ::_thesis: verum
end;
theorem :: AFINSQ_2:71
for cF being complex-valued XFinSequence
for B1, B2 being finite natural-membered set st B1 D) = the_unity_wrt b
proof
let D be non empty set ; ::_thesis: for b being BinOp of D st b is having_a_unity holds
b "**" (<%> D) = the_unity_wrt b
let b be BinOp of D; ::_thesis: ( b is having_a_unity implies b "**" (<%> D) = the_unity_wrt b )
A1: len (<%> D) = 0 ;
assume b is having_a_unity ; ::_thesis: b "**" (<%> D) = the_unity_wrt b
hence b "**" (<%> D) = the_unity_wrt b by A1, Def8; ::_thesis: verum
end;
definition
let D be set ;
let F be XFinSequence of D ^omega ;
func FlattenSeq F -> Element of D ^omega means :Def10: :: AFINSQ_2:def 10
ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & it = g "**" F );
existence
ex b1 being Element of D ^omega ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b1 = g "**" F )
proof
deffunc H1( Element of D ^omega , Element of D ^omega ) -> Element of D ^omega = $1 ^ $2;
consider g being BinOp of (D ^omega) such that
A1: for a, b being Element of D ^omega holds g . (a,b) = H1(a,b) from BINOP_1:sch_4();
take g "**" F ; ::_thesis: ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & g "**" F = g "**" F )
take g ; ::_thesis: ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & g "**" F = g "**" F )
thus ( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & g "**" F = g "**" F ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of D ^omega st ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b1 = g "**" F ) & ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b2 = g "**" F ) holds
b1 = b2
proof
let it1, it2 be Element of D ^omega ; ::_thesis: ( ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & it1 = g "**" F ) & ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & it2 = g "**" F ) implies it1 = it2 )
given g1 being BinOp of (D ^omega) such that A2: for p, q being Element of D ^omega holds g1 . (p,q) = p ^ q and
A3: it1 = g1 "**" F ; ::_thesis: ( for g being BinOp of (D ^omega) holds
( ex p, q being Element of D ^omega st not g . (p,q) = p ^ q or not it2 = g "**" F ) or it1 = it2 )
given g2 being BinOp of (D ^omega) such that A4: for p, q being Element of D ^omega holds g2 . (p,q) = p ^ q and
A5: it2 = g2 "**" F ; ::_thesis: it1 = it2
now__::_thesis:_for_a,_b_being_Element_of_D_^omega_holds_g1_._(a,b)_=_g2_._(a,b)
let a, b be Element of D ^omega ; ::_thesis: g1 . (a,b) = g2 . (a,b)
thus g1 . (a,b) = a ^ b by A2
.= g2 . (a,b) by A4 ; ::_thesis: verum
end;
hence it1 = it2 by A3, A5, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines FlattenSeq AFINSQ_2:def_10_:_
for D being set
for F being XFinSequence of D ^omega
for b3 being Element of D ^omega holds
( b3 = FlattenSeq F iff ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b3 = g "**" F ) );
theorem :: AFINSQ_2:73
for D being set
for d being Element of D ^omega holds FlattenSeq <%d%> = d
proof
let D be set ; ::_thesis: for d being Element of D ^omega holds FlattenSeq <%d%> = d
let d be Element of D ^omega ; ::_thesis: FlattenSeq <%d%> = d
ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & FlattenSeq <%d%> = g "**" <%d%> ) by Def10;
hence FlattenSeq <%d%> = d by Th37; ::_thesis: verum
end;
theorem :: AFINSQ_2:74
for D being set holds FlattenSeq (<%> (D ^omega)) = <%> D
proof
let D be set ; ::_thesis: FlattenSeq (<%> (D ^omega)) = <%> D
consider g being BinOp of (D ^omega) such that
A1: for d1, d2 being Element of D ^omega holds g . (d1,d2) = d1 ^ d2 and
A2: FlattenSeq (<%> (D ^omega)) = g "**" (<%> (D ^omega)) by Def10;
A3: {} is Element of D ^omega by AFINSQ_1:43;
reconsider p = {} as Element of D ^omega by AFINSQ_1:43;
now__::_thesis:_for_a_being_Element_of_D_^omega_holds_
(_g_._({},a)_=_a_&_g_._(a,{})_=_a_)
let a be Element of D ^omega ; ::_thesis: ( g . ({},a) = a & g . (a,{}) = a )
thus g . ({},a) = {} ^ a by A1, A3
.= a ; ::_thesis: g . (a,{}) = a
thus g . (a,{}) = a ^ {} by A1, A3
.= a ; ::_thesis: verum
end;
then A4: p is_a_unity_wrt g by BINOP_1:3;
then g is having_a_unity by SETWISEO:def_2;
then g "**" (<%> (D ^omega)) = the_unity_wrt g by Th72;
hence FlattenSeq (<%> (D ^omega)) = <%> D by A2, A4, BINOP_1:def_8; ::_thesis: verum
end;
theorem Th75: :: AFINSQ_2:75
for D being set
for F, G being XFinSequence of D ^omega holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)
proof
let D be set ; ::_thesis: for F, G being XFinSequence of D ^omega holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)
let F, G be XFinSequence of D ^omega ; ::_thesis: FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)
consider g being BinOp of (D ^omega) such that
A1: for d1, d2 being Element of D ^omega holds g . (d1,d2) = d1 ^ d2 and
A2: FlattenSeq (F ^ G) = g "**" (F ^ G) by Def10;
now__::_thesis:_for_a,_b,_c_being_Element_of_D_^omega_holds_g_._(a,(g_._(b,c)))_=_g_._((g_._(a,b)),c)
let a, b, c be Element of D ^omega ; ::_thesis: g . (a,(g . (b,c))) = g . ((g . (a,b)),c)
thus g . (a,(g . (b,c))) = a ^ (g . (b,c)) by A1
.= a ^ (b ^ c) by A1
.= (a ^ b) ^ c by AFINSQ_1:27
.= (g . (a,b)) ^ c by A1
.= g . ((g . (a,b)),c) by A1 ; ::_thesis: verum
end;
then A3: g is associative by BINOP_1:def_3;
A4: {} is Element of D ^omega by AFINSQ_1:43;
reconsider p = {} as Element of D ^omega by AFINSQ_1:43;
now__::_thesis:_for_a_being_Element_of_D_^omega_holds_
(_g_._({},a)_=_a_&_g_._(a,{})_=_a_)
let a be Element of D ^omega ; ::_thesis: ( g . ({},a) = a & g . (a,{}) = a )
thus g . ({},a) = {} ^ a by A1, A4
.= a ; ::_thesis: g . (a,{}) = a
thus g . (a,{}) = a ^ {} by A1, A4
.= a ; ::_thesis: verum
end;
then p is_a_unity_wrt g by BINOP_1:3;
then ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) by SETWISEO:def_2;
hence FlattenSeq (F ^ G) = g . ((g "**" F),(g "**" G)) by A2, A3, Th41
.= (g "**" F) ^ (g "**" G) by A1
.= (FlattenSeq F) ^ (g "**" G) by A1, Def10
.= (FlattenSeq F) ^ (FlattenSeq G) by A1, Def10 ;
::_thesis: verum
end;
theorem :: AFINSQ_2:76
for D being set
for p, q being Element of D ^omega holds FlattenSeq <%p,q%> = p ^ q
proof
let D be set ; ::_thesis: for p, q being Element of D ^omega holds FlattenSeq <%p,q%> = p ^ q
let p, q be Element of D ^omega ; ::_thesis: FlattenSeq <%p,q%> = p ^ q
consider g being BinOp of (D ^omega) such that
A1: for d1, d2 being Element of D ^omega holds g . (d1,d2) = d1 ^ d2 and
A2: FlattenSeq <%p,q%> = g "**" <%p,q%> by Def10;
thus FlattenSeq <%p,q%> = g . (p,q) by A2, Th38
.= p ^ q by A1 ; ::_thesis: verum
end;
theorem :: AFINSQ_2:77
for D being set
for p, q, r being Element of D ^omega holds FlattenSeq <%p,q,r%> = (p ^ q) ^ r
proof
let D be set ; ::_thesis: for p, q, r being Element of D ^omega holds FlattenSeq <%p,q,r%> = (p ^ q) ^ r
let p, q, r be Element of D ^omega ; ::_thesis: FlattenSeq <%p,q,r%> = (p ^ q) ^ r
consider g being BinOp of (D ^omega) such that
A1: for d1, d2 being Element of D ^omega holds g . (d1,d2) = d1 ^ d2 and
A2: FlattenSeq <%p,q,r%> = g "**" <%p,q,r%> by Def10;
thus FlattenSeq <%p,q,r%> = g . ((g . (p,q)),r) by A2, Th39
.= (g . (p,q)) ^ r by A1
.= (p ^ q) ^ r by A1 ; ::_thesis: verum
end;
theorem Th78: :: AFINSQ_2:78
for p, q being XFinSequence st p c= q holds
p ^ (q /^ (len p)) = q
proof
let p, q be XFinSequence; ::_thesis: ( p c= q implies p ^ (q /^ (len p)) = q )
assume A1: p c= q ; ::_thesis: p ^ (q /^ (len p)) = q
A2: (len p) + (len (q /^ (len p))) = (len p) + ((len q) -' (len p)) by Def2
.= ((len q) + (len p)) -' (len p) by A1, NAT_1:43, NAT_D:38
.= dom q by NAT_D:34 ;
A3: for k being Nat st k in dom p holds
q . k = p . k by A1, GRFUNC_1:2;
for k being Nat st k in dom (q /^ (len p)) holds
q . ((len p) + k) = (q /^ (len p)) . k by Def2;
hence p ^ (q /^ (len p)) = q by A2, A3, AFINSQ_1:def_3; ::_thesis: verum
end;
theorem Th79: :: AFINSQ_2:79
for p, q being XFinSequence st p c= q holds
ex r being XFinSequence st p ^ r = q
proof
let p, q be XFinSequence; ::_thesis: ( p c= q implies ex r being XFinSequence st p ^ r = q )
assume A1: p c= q ; ::_thesis: ex r being XFinSequence st p ^ r = q
take r = q /^ (len p); ::_thesis: p ^ r = q
thus p ^ r = q by A1, Th78; ::_thesis: verum
end;
theorem Th80: :: AFINSQ_2:80
for D being non empty set
for p, q being XFinSequence of D st p c= q holds
ex r being XFinSequence of D st p ^ r = q
proof
let D be non empty set ; ::_thesis: for p, q being XFinSequence of D st p c= q holds
ex r being XFinSequence of D st p ^ r = q
let p, q be XFinSequence of D; ::_thesis: ( p c= q implies ex r being XFinSequence of D st p ^ r = q )
assume p c= q ; ::_thesis: ex r being XFinSequence of D st p ^ r = q
then consider r being XFinSequence such that
A1: p ^ r = q by Th79;
reconsider r = r as XFinSequence of D by A1, AFINSQ_1:31;
take r ; ::_thesis: p ^ r = q
thus p ^ r = q by A1; ::_thesis: verum
end;
theorem :: AFINSQ_2:81
for q, p, r being XFinSequence st q c= r holds
p ^ q c= p ^ r
proof
let q, p, r be XFinSequence; ::_thesis: ( q c= r implies p ^ q c= p ^ r )
assume q c= r ; ::_thesis: p ^ q c= p ^ r
then consider s being XFinSequence such that
A1: q ^ s = r by Th79;
p ^ q c= (p ^ q) ^ s by AFINSQ_1:74;
hence p ^ q c= p ^ r by A1, AFINSQ_1:27; ::_thesis: verum
end;
theorem :: AFINSQ_2:82
for D being set
for F, G being XFinSequence of D ^omega st F c= G holds
FlattenSeq F c= FlattenSeq G
proof
let D be set ; ::_thesis: for F, G being XFinSequence of D ^omega st F c= G holds
FlattenSeq F c= FlattenSeq G
let F, G be XFinSequence of D ^omega ; ::_thesis: ( F c= G implies FlattenSeq F c= FlattenSeq G )
assume F c= G ; ::_thesis: FlattenSeq F c= FlattenSeq G
then consider F9 being XFinSequence of D ^omega such that
A1: F ^ F9 = G by Th80;
(FlattenSeq F) ^ (FlattenSeq F9) = FlattenSeq G by A1, Th75;
hence FlattenSeq F c= FlattenSeq G by AFINSQ_1:74; ::_thesis: verum
end;
registration
let p be XFinSequence;
let q be non empty XFinSequence;
clusterp ^ q -> non empty ;
coherence
not p ^ q is empty by AFINSQ_1:30;
clusterq ^ p -> non empty ;
coherence
not q ^ p is empty by AFINSQ_1:30;
end;
theorem :: AFINSQ_2:83
for x being set
for p being XFinSequence holds CutLastLoc (p ^ <%x%>) = p
proof
let x be set ; ::_thesis: for p being XFinSequence holds CutLastLoc (p ^ <%x%>) = p
let p be XFinSequence; ::_thesis: CutLastLoc (p ^ <%x%>) = p
set q = CutLastLoc (p ^ <%x%>);
A1: (len (p ^ <%x%>)) -' 1 = ((len p) + 1) -' 1 by AFINSQ_1:75
.= len p by NAT_D:34 ;
A2: dom (p ^ <%x%>) = len (p ^ <%x%>)
.= (len p) + 1 by AFINSQ_1:75
.= (dom p) \/ {(len p)} by AFINSQ_1:2 ;
A3: not len p in dom p ;
LastLoc (p ^ <%x%>) = (len (p ^ <%x%>)) -' 1 by AFINSQ_1:70;
hence A4: dom (CutLastLoc (p ^ <%x%>)) = (dom (p ^ <%x%>)) \ {(len p)} by A1, VALUED_1:36
.= dom p by A2, A3, ZFMISC_1:117 ;
:: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom (CutLastLoc (p ^ <%x%>)) or (CutLastLoc (p ^ <%x%>)) . b1 = p . b1 )
let y be set ; ::_thesis: ( not y in dom (CutLastLoc (p ^ <%x%>)) or (CutLastLoc (p ^ <%x%>)) . y = p . y )
assume A5: y in dom (CutLastLoc (p ^ <%x%>)) ; ::_thesis: (CutLastLoc (p ^ <%x%>)) . y = p . y
A6: p c= p ^ <%x%> by AFINSQ_1:74;
thus (CutLastLoc (p ^ <%x%>)) . y = (p ^ <%x%>) . y by A5, GRFUNC_1:2
.= p . y by A5, A4, A6, GRFUNC_1:2 ; ::_thesis: verum
end;