let D be non empty set ; :: thesis: for f being FinSequence of D
for d, e being Element of D
for i being Element of NAT holds f +* (i,(f /. i)) = f
let f be FinSequence of D; :: thesis: for d, e being Element of D
for i being Element of NAT holds f +* (i,(f /. i)) = f
let d, e be Element of D; :: thesis: for i being Element of NAT holds f +* (i,(f /. i)) = f
let i be Element of 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 Th37 ;
:: thesis: verum

end;

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

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

end;

end;