let f1, f2 be integer-valued FinSequence; :: thesis: ( len f1 = len f2 & ( for n being Nat st 1 <= n & n <= len f1 holds
f1 . n divides f2 . n ) implies Product f1 divides Product f2 )
assume that
A1: len f1 = len f2 and
A2: for n being Nat st 1 <= n & n <= len f1 holds
f1 . n divides f2 . n ; :: thesis: Product f1 divides Product f2

per cases ( len f1 = 0 or 0 + 1 <= len f1 ) by NAT_1:13;

suppose len f1 = 0 ; :: thesis: Product f1 divides Product f2

then ( f1 = {} & f2 = {} ) by A1;
hence Product f1 divides Product f2 ; :: thesis: verum

end;

suppose A3: 0 + 1 <= len f1 ; :: thesis: Product f1 divides Product f2

defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f1 implies Product (f1 | $1) divides Product (f2 | $1) );
A4: S₁[ 0 ] ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A6: S₁[k] and
A7: 1 <= k + 1 and
A8: k + 1 <= len f1 ; :: thesis: Product (f1 | (k + 1)) divides Product (f2 | (k + 1))
A9: k + 0 < k + 1 by XREAL_1:8;

per cases ( k = 0 or k > 0 ) ;

suppose A10: k = 0 ; :: thesis: Product (f1 | (k + 1)) divides Product (f2 | (k + 1))

not f1 is empty by A8;
then A11: f1 | 1 = <*(f1 . 1)*> by FINSEQ_5:20;
not f2 is empty by A1, A8;
then f2 | 1 = <*(f2 . 1)*> by FINSEQ_5:20;
hence Product (f1 | (k + 1)) divides Product (f2 | (k + 1)) by A2, A3, A10, A11; :: thesis: verum

end;

suppose k > 0 ; :: thesis: Product (f1 | (k + 1)) divides Product (f2 | (k + 1))

then A12: k >= 0 + 1 by NAT_1:13;
f1 | (k + 1) = (f1 | k) ^ <*(f1 . (k + 1))*> by A8, INT_6:5;
then A13: Product (f1 | (k + 1)) = (Product (f1 | k)) * (f1 . (k + 1)) by RVSUM_1:96;
f2 | (k + 1) = (f2 | k) ^ <*(f2 . (k + 1))*> by A1, A8, INT_6:5;
then A14: Product (f2 | (k + 1)) = (Product (f2 | k)) * (f2 . (k + 1)) by RVSUM_1:96;
f1 . (k + 1) divides f2 . (k + 1) by A2, A7, A8;
hence Product (f1 | (k + 1)) divides Product (f2 | (k + 1)) by A6, A8, A9, A12, A13, A14, NEWTON02:2, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A15: for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
( f1 | (len f1) = f1 & f2 | (len f2) = f2 ) by FINSEQ_3:113;
hence Product f1 divides Product f2 by A1, A3, A15; :: thesis: verum

end;

end;