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 that
A1: i <> 0 and
A2: i <= len f ; :: thesis: (f ^ g) /. i = f /. 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 f by A2, FINSEQ_3:25;
hence (f ^ g) /. i = f /. i by Lm1; :: thesis: verum