let D be non empty set ; :: thesis: for f being FinSequence of D
for d, e being Element of D
for i being Nat holds f +* (i,(f /. i)) = f
let f be FinSequence of D; :: thesis: for d, e being Element of D
for i being Nat holds f +* (i,(f /. i)) = f
let d, e be Element of D; :: thesis: for i being Nat holds f +* (i,(f /. i)) = f
let i be Nat; :: thesis: f +* (i,(f /. i)) = f

per cases ( i in dom f or not i in dom f ) ;

suppose i in dom f ; :: thesis: f +* (i,(f /. i)) = f

hence f +* (i,(f /. i)) = f +* (i,(f . i)) by PARTFUN1:def 6
.= f by Th34 ;
:: thesis: verum

end;

suppose not i in dom f ; :: thesis: f +* (i,(f /. i)) = f

hence f +* (i,(f /. i)) = f by Def2; :: thesis: verum

end;

end;