let i, j be Nat; :: thesis: for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) * (f /. j))*> is being_a_generation_from_squares
let R be non empty doubleLoopStr ; :: thesis: for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) * (f /. j))*> is being_a_generation_from_squares
let f be FinSequence of R; :: thesis: ( f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f implies f ^ <*((f /. i) * (f /. j))*> is being_a_generation_from_squares )
assume that
A1: f is being_a_generation_from_squares and
A2: i <> 0 and
A3: i <= len f and
A4: j <> 0 and
A5: j <= len f ; :: thesis: f ^ <*((f /. i) * (f /. j))*> is being_a_generation_from_squares
set g = f ^ <*((f /. i) * (f /. j))*>;
A6: len (f ^ <*((f /. i) * (f /. j))*>) = (len f) + (len <*((f /. i) * (f /. j))*>) by FINSEQ_1:22
.= (len f) + 1 by Lm2 ;
A7: for n being Nat st n <> 0 & n <= len (f ^ <*((f /. i) * (f /. j))*>) & not (f ^ <*((f /. i) * (f /. j))*>) /. n is being_an_amalgam_of_squares holds
ex i, j being Nat st
( ( (f ^ <*((f /. i) * (f /. j))*>) /. n = ((f ^ <*((f /. i) * (f /. j))*>) /. i) * ((f ^ <*((f /. i) * (f /. j))*>) /. j) or (f ^ <*((f /. i) * (f /. j))*>) /. n = ((f ^ <*((f /. i) * (f /. j))*>) /. i) + ((f ^ <*((f /. i) * (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) len f <> 0 by A1;
then (len f) + (len <*((f /. i) * (f /. j))*>) <> 0 ;
then len (f ^ <*((f /. i) * (f /. j))*>) <> 0 by FINSEQ_1:22;
hence f ^ <*((f /. i) * (f /. j))*> is being_a_generation_from_squares by A7; :: thesis: verum