let n be Nat; for x being Element of REAL n
for f being FinSequence st x <> 0* n & x = f holds
ex i being Element of NAT st
( 1 <= i & i <= n & f . i <> 0 )
let x be Element of REAL n; for f being FinSequence st x <> 0* n & x = f holds
ex i being Element of NAT st
( 1 <= i & i <= n & f . i <> 0 )
let f be FinSequence; ( x <> 0* n & x = f implies ex i being Element of NAT st
( 1 <= i & i <= n & f . i <> 0 ) )
assume that
A1:
x <> 0* n
and
A2:
x = f
; ex i being Element of NAT st
( 1 <= i & i <= n & f . i <> 0 )
A3:
len f = n
by A2, CARD_1:def 7;
assume A4:
for i being Element of NAT holds
( not 1 <= i or not i <= n or not f . i <> 0 )
; contradiction
for z being object holds
( z in f iff ex x, y being object st
( x in Seg n & y in {0} & z = [x,y] ) )
proof
let z be
object ;
( z in f iff ex x, y being object st
( x in Seg n & y in {0} & z = [x,y] ) )
hereby ( ex x, y being object st
( x in Seg n & y in {0} & z = [x,y] ) implies z in f )
assume A5:
z in f
;
ex x, y being object st
( x in Seg n & y in {0} & z = [x,y] )then consider x0,
y0 being
object such that A6:
z = [x0,y0]
by RELAT_1:def 1;
A7:
y0 = f . x0
by A5, A6, FUNCT_1:1;
A8:
x0 in dom f
by A5, A6, XTUPLE_0:def 12;
then reconsider n1 =
x0 as
Element of
NAT ;
A9:
x0 in Seg (len f)
by A8, FINSEQ_1:def 3;
then
( 1
<= n1 &
n1 <= len f )
by FINSEQ_1:1;
then
f . n1 = 0
by A3, A4;
then
y0 in {0}
by A7, TARSKI:def 1;
hence
ex
x,
y being
object st
(
x in Seg n &
y in {0} &
z = [x,y] )
by A3, A6, A9;
verum
end;
given x,
y being
object such that A10:
x in Seg n
and A11:
y in {0}
and A12:
z = [x,y]
;
z in f
reconsider n1 =
x as
Element of
NAT by A10;
A13:
n1 <= n
by A10, FINSEQ_1:1;
A14:
x in dom f
by A3, A10, FINSEQ_1:def 3;
(
y = 0 & 1
<= n1 )
by A10, A11, FINSEQ_1:1, TARSKI:def 1;
then
y = f . x
by A4, A13;
hence
z in f
by A12, A14, FUNCT_1:1;
verum
end;
then
f = [:(Seg n),{0}:]
by ZFMISC_1:def 2;
hence
contradiction
by A1, A2, FUNCOP_1:def 2; verum