let D be set ; :: thesis: for f being FinSequence of D
for i being Element of NAT st i >= len f holds
f /^ i = <*> D
let f be FinSequence of D; :: thesis: for i being Element of NAT st i >= len f holds
f /^ i = <*> D
let i be Element of NAT ; :: thesis: ( i >= len f implies f /^ i = <*> D )
assume A1: i >= len f ; :: thesis: f /^ i = <*> D

per cases ( i > len f or i = len f ) by A1, XXREAL_0:1;

suppose i > len f ; :: thesis: f /^ i = <*> D

hence f /^ i = <*> D by RFINSEQ:def 2; :: thesis: verum

end;

suppose A2: i = len f ; :: thesis: f /^ i = <*> D

then len (f /^ i) = (len f) - i by RFINSEQ:def 2
.= 0 by A2 ;
hence f /^ i = <*> D ; :: thesis: verum

end;

end;