let fp be FinSequence of NAT ; :: thesis: for a being Nat
for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds
fp . b divides Product (Del (fp,a))
let a be Nat; :: thesis: for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds
fp . b divides Product (Del (fp,a))
let b be Element of NAT ; :: thesis: ( a in dom fp & b in dom fp & a <> b & len fp >= 1 implies fp . b divides Product (Del (fp,a)) )
assume that
A1: a in dom fp and
A2: b in dom fp and
A3: a <> b and
A4: len fp >= 1 ; :: thesis: fp . b divides Product (Del (fp,a))
consider n being Nat such that
A5: len fp = n + 1 by A4, NAT_1:6;
A6: a <= n + 1 by A1, A5, FINSEQ_3:25;
A7: a >= 1 by A1, FINSEQ_3:25;
A8: b >= 1 by A2, FINSEQ_3:25;
A9: (len (Del (fp,a))) + 1 = n + 1 by A1, A5, WSIERP_1:def 1;
A10: b <= n + 1 by A2, A5, FINSEQ_3:25;

per cases ( a <= n or a = n + 1 ) by A6, NAT_1:8;

suppose A11: a <= n ; :: thesis: fp . b divides Product (Del (fp,a))

per cases ( b < a or a < b ) by A3, XXREAL_0:1;

suppose A12: b < a ; :: thesis: fp . b divides Product (Del (fp,a))

then b <= n by A11, XXREAL_0:2;
then A13: b in dom (Del (fp,a)) by A8, A9, FINSEQ_3:25;
(Del (fp,a)) . b = fp . b by A1, A12, WSIERP_1:def 1;
hence fp . b divides Product (Del (fp,a)) by A13, Th32; :: thesis: verum

end;

suppose A14: a < b ; :: thesis: fp . b divides Product (Del (fp,a))

then b >= a + 1 by NAT_1:13;
then b - 1 >= a by XREAL_1:19;
then b -' 1 >= a by A8, XREAL_1:233;
then A15: (Del (fp,a)) . (b -' 1) = fp . ((b -' 1) + 1) by A1, WSIERP_1:def 1;
b > 1 by A7, A14, XXREAL_0:2;
then b - 1 > 0 by XREAL_1:50;
then b -' 1 > 0 by A8, XREAL_1:233;
then A16: b -' 1 >= 1 by Lm7;
b - 1 <= (n + 1) - 1 by A10, XREAL_1:9;
then b -' 1 <= n by A8, XREAL_1:233;
then b -' 1 in dom (Del (fp,a)) by A9, A16, FINSEQ_3:25;
then (Del (fp,a)) . (b -' 1) divides Product (Del (fp,a)) by Th32;
hence fp . b divides Product (Del (fp,a)) by A8, A15, XREAL_1:235; :: thesis: verum

end;

end;

end;

suppose A17: a = n + 1 ; :: thesis: fp . b divides Product (Del (fp,a))

then b < n + 1 by A3, A10, XXREAL_0:1;
then b <= n by NAT_1:13;
then A18: b in dom (Del (fp,a)) by A8, A9, FINSEQ_3:25;
b < a by A3, A10, A17, XXREAL_0:1;
then (Del (fp,a)) . b = fp . b by A1, WSIERP_1:def 1;
hence fp . b divides Product (Del (fp,a)) by A18, Th32; :: thesis: verum

end;

end;