let i be Nat; :: thesis: for D being non empty set
for f, g being FinSequence of D st i in dom f holds
(f ^ g) /. i = f /. i
let D be non empty set ; :: thesis: for f, g being FinSequence of D st i in dom f holds
(f ^ g) /. i = f /. i
let f, g be FinSequence of D; :: thesis: ( i in dom f implies (f ^ g) /. i = f /. i )
assume A1: i in dom f ; :: thesis: (f ^ g) /. i = f /. i
dom f c= dom (f ^ g) by FINSEQ_1:26;
hence (f ^ g) /. i = (f ^ g) . i by A1, PARTFUN1:def 6
.= f . i by A1, FINSEQ_1:def 7
.= f /. i by A1, PARTFUN1:def 6 ;
:: thesis: verum