let n, i be Element of NAT ; :: thesis: ( i <= n implies (0* n) | i = 0* i )
assume A1: i <= n ; :: thesis: (0* n) | i = 0* i
then i <= len (0* n) by CARD_1:def 7;
then A2: len ((0* n) | i) = i by FINSEQ_1:59;
A3: for j being Nat st 1 <= j & j <= i holds
((0* n) | i) . j = (0* i) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= i implies ((0* n) | i) . j = (0* i) . j )
assume that
A4: 1 <= j and
A5: j <= i ; :: thesis: ((0* n) | i) . j = (0* i) . j
j <= n by A1, A5, XXREAL_0:2;
then A6: j in Seg n by A4, FINSEQ_1:1;
A7: ((0* n) | i) . j = (n |-> 0) . j by A5, FINSEQ_3:112
.= 0 by A6, FUNCOP_1:7 ;
j in Seg i by A4, A5, FINSEQ_1:1;
hence ((0* n) | i) . j = (0* i) . j by A7, FUNCOP_1:7; :: thesis: verum

end;

i = len (0* i) by CARD_1:def 7;
hence (0* n) | i = 0* i by A2, A3, FINSEQ_1:14; :: thesis: verum