let u be Element of (TOP-REAL 3); :: thesis: for uf being FinSequence of F_Real st u = uf & <*uf*> @ = <*<*0*>,<*0*>,<*0*>*> holds
u = 0. (TOP-REAL 3)
let uf be FinSequence of F_Real; :: thesis: ( u = uf & <*uf*> @ = <*<*0*>,<*0*>,<*0*>*> implies u = 0. (TOP-REAL 3) )
assume that
A1: u = uf and
A2: <*uf*> @ = <*<*0*>,<*0*>,<*0*>*> ; :: thesis: u = 0. (TOP-REAL 3)
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A3: u in 3 -tuples_on REAL by EUCLID:def 1;
then A4: len uf = 3 by A1, FINSEQ_2:133;
<*uf*> @ = <*<*(uf . 1)*>,<*(uf . 2)*>,<*(uf . 3)*>*> by A3, A1, FINSEQ_2:133, Th63;
then ( <*(uf . 1)*> = <*0*> & <*(uf . 2)*> = <*0*> & <*(uf . 3)*> = <*0*> ) by A2, FINSEQ_1:78;
then ( uf . 1 = 0 & uf . 2 = 0 & uf . 3 = 0 ) by FINSEQ_1:76;
hence u = 0. (TOP-REAL 3) by A1, A4, FINSEQ_1:45, EUCLID_5:4; :: thesis: verum