scheme :: FLEXARY1:sch 1
TT{ F₁() -> complex-valued FinSequence, F₂() -> complex-valued FinSequence, F₃() -> Nat, F₄() -> Nat, F₅() -> non zero Nat, F₆() -> non zero Nat } :

(F₁(),F₃()) +... = (F₂(),F₄()) +...

provided

A1: for j being Nat holds (F₁(),(F₃() + (j * F₅()))) +...+ (F₁(),((F₃() + (j * F₅())) + (F₅() -' 1))) = (F₂(),(F₄() + (j * F₆()))) +...+ (F₂(),((F₄() + (j * F₆())) + (F₆() -' 1)))