let n be 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 k in Seg (len R) by FINSEQ_1:1;
then k in dom R by FINSEQ_1:def 3;
then A3: R . k = 0 by A1;
thus R . k = (n |-> 0) . k by A3; :: thesis: verum

end;

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