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

.= len (n |-> 0) by CARD_1:def 7 ;

hence R = n |-> 0 by A2, FINSEQ_1:14; :: thesis: verum

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

len R =
n
by CARD_1:def 7
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;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

.= len (n |-> 0) by CARD_1:def 7 ;

hence R = n |-> 0 by A2, FINSEQ_1:14; :: thesis: verum