let n be Element of NAT ; :: thesis: for R being Element of n -tuples_on REAL st ( for i being Element of NAT st i in dom R holds
0 = R . i ) holds
R = n |-> 0
let R be Element of n -tuples_on REAL ; :: thesis: ( ( for i being Element of NAT st i in dom R holds
0 = R . i ) implies R = n |-> 0 )
assume A1: for i being Element of NAT st i in dom R holds
0 = R . i ; :: thesis: R = n |-> 0
A2: for k being Nat st 1 <= k & k <= len R holds
R . k = (n |-> 0 ) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len R implies R . k = (n |-> 0 ) . k )
assume ( 1 <= k & k <= len R ) ; :: thesis: R . k = (n |-> 0 ) . k
then A3: k in Seg (len R) by FINSEQ_1:3;
then k in dom R by FINSEQ_1:def 3;
then A4: R . k = 0 by A1;
k in Seg n by A3, FINSEQ_1:def 18;
hence R . k = (n |-> 0 ) . k by A4, FUNCOP_1:13; :: thesis: verum

end;

len R = n by FINSEQ_1:def 18
.= len (n |-> 0 ) by FINSEQ_1:def 18 ;
hence R = n |-> 0 by A2, FINSEQ_1:18; :: thesis: verum