defpred S₁[ Nat] means (F₁(),F₃()) +...+ (F₁(),((F₃() + ($1 * F₅())) + (F₅() -' 1))) = (F₂(),F₄()) +...+ (F₂(),((F₄() + ($1 * F₆())) + (F₆() -' 1)));
A2: S₁[ 0 ] by A1;
A3: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
set j1 = j + 1;
A4: ((F₁(),F₃()) +...+ (F₁(),((F₃() + (j * F₅())) + (F₅() -' 1)))) + ((F₁(),(F₃() + ((j + 1) * F₅()))) +...+ (F₁(),((F₃() + ((j + 1) * F₅())) + (F₅() -' 1)))) = (F₁(),F₃()) +...+ (F₁(),((F₃() + ((j + 1) * F₅())) + (F₅() -' 1)))

proof

A5: F₃() <= F₃() + ((j * F₅()) + (F₅() -' 1)) by NAT_1:11;
(F₅() -' 1) + 1 = F₅() by NAT_1:14, XREAL_1:235;
then A6: ((F₃() + (j * F₅())) + (F₅() -' 1)) + 1 = F₃() + ((j + 1) * F₅()) ;
F₃() + ((j + 1) * F₅()) <= F₃() + (((j + 1) * F₅()) + (F₅() -' 1)) by NAT_1:11, XREAL_1:6;
then (F₃() + (j * F₅())) + (F₅() -' 1) <= F₃() + (((j + 1) * F₅()) + (F₅() -' 1)) by A6, NAT_1:13;
hence ((F₁(),F₃()) +...+ (F₁(),((F₃() + (j * F₅())) + (F₅() -' 1)))) + ((F₁(),(F₃() + ((j + 1) * F₅()))) +...+ (F₁(),((F₃() + ((j + 1) * F₅())) + (F₅() -' 1)))) = (F₁(),F₃()) +...+ (F₁(),((F₃() + ((j + 1) * F₅())) + (F₅() -' 1))) by Th14, A5, A6; :: thesis: verum

end;

((F₂(),F₄()) +...+ (F₂(),((F₄() + (j * F₆())) + (F₆() -' 1)))) + ((F₂(),(F₄() + ((j + 1) * F₆()))) +...+ (F₂(),((F₄() + ((j + 1) * F₆())) + (F₆() -' 1)))) = (F₂(),F₄()) +...+ (F₂(),((F₄() + ((j + 1) * F₆())) + (F₆() -' 1)))

proof

A7: F₄() <= F₄() + ((j * F₆()) + (F₆() -' 1)) by NAT_1:11;
(F₆() -' 1) + 1 = F₆() by NAT_1:14, XREAL_1:235;
then A8: ((F₄() + (j * F₆())) + (F₆() -' 1)) + 1 = F₄() + ((j + 1) * F₆()) ;
F₄() + ((j + 1) * F₆()) <= F₄() + (((j + 1) * F₆()) + (F₆() -' 1)) by NAT_1:11, XREAL_1:6;
then (F₄() + (j * F₆())) + (F₆() -' 1) <= F₄() + (((j + 1) * F₆()) + (F₆() -' 1)) by A8, NAT_1:13;
hence ((F₂(),F₄()) +...+ (F₂(),((F₄() + (j * F₆())) + (F₆() -' 1)))) + ((F₂(),(F₄() + ((j + 1) * F₆()))) +...+ (F₂(),((F₄() + ((j + 1) * F₆())) + (F₆() -' 1)))) = (F₂(),F₄()) +...+ (F₂(),((F₄() + ((j + 1) * F₆())) + (F₆() -' 1))) by Th14, A7, A8; :: thesis: verum

end;

hence ( S₁[j] implies S₁[j + 1] ) by A1, A4; :: thesis: verum

end;

A9: for j being Nat holds S₁[j] from NAT_1:sch 2(A2, A3);

per cases ( len F₁() >= len F₂() or len F₂() >= len F₁() ) ;

suppose A10: len F₁() >= len F₂() ; :: thesis: (F₁(),F₃()) +... = (F₂(),F₄()) +...

set l = len F₁();
(len F₁()) * 1 <= (len F₁()) * F₅() by NAT_1:14, XREAL_1:64;
then len F₁() <= ((len F₁()) * F₅()) + (F₃() + (F₅() -' 1)) by XREAL_1:38;
then A11: (F₁(),F₃()) +...+ (F₁(),((F₃() + ((len F₁()) * F₅())) + (F₅() -' 1))) = (F₁(),F₃()) +... by Th16;
A12: (len F₂()) * F₆() <= (len F₁()) * F₆() by A10, XREAL_1:64;
(len F₂()) * 1 <= (len F₂()) * F₆() by NAT_1:14, XREAL_1:64;
then len F₂() <= (len F₁()) * F₆() by A12, XXREAL_0:2;
then len F₂() <= ((len F₁()) * F₆()) + (F₄() + (F₆() -' 1)) by XREAL_1:38;
then ( (F₂(),F₄()) +...+ (F₂(),((F₄() + ((len F₁()) * F₆())) + (F₆() -' 1))) = (F₂(),F₄()) +...+ (F₂(),(len F₂())) & (F₂(),F₄()) +...+ (F₂(),(len F₂())) = (F₂(),F₄()) +... ) by Th16;
hence (F₁(),F₃()) +... = (F₂(),F₄()) +... by A9, A11; :: thesis: verum

end;

suppose A13: len F₂() >= len F₁() ; :: thesis: (F₁(),F₃()) +... = (F₂(),F₄()) +...

set l = len F₂();
(len F₂()) * 1 <= (len F₂()) * F₆() by NAT_1:14, XREAL_1:64;
then len F₂() <= ((len F₂()) * F₆()) + (F₄() + (F₆() -' 1)) by XREAL_1:38;
then A14: (F₂(),F₄()) +...+ (F₂(),((F₄() + ((len F₂()) * F₆())) + (F₆() -' 1))) = (F₂(),F₄()) +... by Th16;
A15: (len F₁()) * F₅() <= (len F₂()) * F₅() by A13, XREAL_1:64;
(len F₁()) * 1 <= (len F₁()) * F₅() by NAT_1:14, XREAL_1:64;
then len F₁() <= (len F₂()) * F₅() by A15, XXREAL_0:2;
then len F₁() <= ((len F₂()) * F₅()) + (F₃() + (F₅() -' 1)) by XREAL_1:38;
then (F₁(),F₃()) +...+ (F₁(),((F₃() + ((len F₂()) * F₅())) + (F₅() -' 1))) = (F₁(),F₃()) +... by Th16;
hence (F₁(),F₃()) +... = (F₂(),F₄()) +... by A9, A14; :: thesis: verum

end;

end;