let n be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: ( x <> 0* n & x = f implies ex i being Element of NAT st
( 1 <= i & i <= n & f . i <> 0 ) )
assume A1:
( x <> 0* n & x = f )
; :: thesis: ex i being Element of NAT st
( 1 <= i & i <= n & f . i <> 0 )
then A2:
len f = n
by FINSEQ_1:def 18;
assume A3:
for i being Element of NAT holds
( not 1 <= i or not i <= n or not f . i <> 0 )
; :: thesis: contradiction
for z being set holds
( z in f iff ex x, y being set st
( x in Seg n & y in {0 } & z = [x,y] ) )
proof
let z be
set ;
:: thesis: ( z in f iff ex x, y being set st
( x in Seg n & y in {0 } & z = [x,y] ) )
hereby :: thesis: ( ex x, y being set st
( x in Seg n & y in {0 } & z = [x,y] ) implies z in f )
assume A4:
z in f
;
:: thesis: ex x, y being set st
( x in Seg n & y in {0 } & z = [x,y] )then consider x0,
y0 being
set such that A5:
z = [x0,y0]
by RELAT_1:def 1;
A6:
x0 in dom f
by A4, A5, RELAT_1:def 4;
then A7:
x0 in Seg (len f)
by FINSEQ_1:def 3;
reconsider n1 =
x0 as
Element of
NAT by A6;
( 1
<= n1 &
n1 <= len f )
by A7, FINSEQ_1:3;
then A8:
f . n1 = 0
by A2, A3;
y0 = f . x0
by A4, A5, FUNCT_1:8;
then
y0 in {0 }
by A8, TARSKI:def 1;
hence
ex
x,
y being
set st
(
x in Seg n &
y in {0 } &
z = [x,y] )
by A2, A5, A7;
:: thesis: verum
end;
given x,
y being
set such that A9:
(
x in Seg n &
y in {0 } &
z = [x,y] )
;
:: thesis: z in f
A10:
y = 0
by A9, TARSKI:def 1;
reconsider n1 =
x as
Element of
NAT by A9;
( 1
<= n1 &
n1 <= n )
by A9, FINSEQ_1:3;
then
(
x in dom f &
y = f . x )
by A2, A3, A9, A10, FINSEQ_1:def 3;
hence
z in f
by A9, FUNCT_1:8;
:: thesis: verum
end;
then
f = [:(Seg n),{0 }:]
by ZFMISC_1:def 2;
hence
contradiction
by A1, FUNCOP_1:def 2; :: thesis: verum