let i be Nat; :: thesis: for R being non empty doubleLoopStr
for f, g being FinSequence of R st i <> 0 & i <= len f holds
(f ^ g) /. i = f /. i
let R be non empty doubleLoopStr ; :: thesis: for f, g being FinSequence of R st i <> 0 & i <= len f holds
(f ^ g) /. i = f /. i
let f, g be FinSequence of R; :: thesis: ( i <> 0 & i <= len f implies (f ^ g) /. i = f /. i )
assume A1: ( i <> 0 & i <= len f ) ; :: thesis: (f ^ g) /. i = f /. i
then ( 0 <> i & 0 <= i ) by NAT_1:2;
then 0 < i by XXREAL_0:1;
then 0 + 1 <= i by NAT_1:13;
then i in dom f by A1, FINSEQ_3:27;
hence (f ^ g) /. i = f /. i by Lm1; :: thesis: verum