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