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