let a be Nat; :: thesis: for fp being FinSequence of NAT st a in dom fp holds
(Product fp) / (fp . a) is Element of NAT
let fp be FinSequence of NAT ; :: thesis: ( a in dom fp implies (Product fp) / (fp . a) is Element of NAT )
assume a in dom fp ; :: thesis: (Product fp) / (fp . a) is Element of NAT
then consider fs1, fs2 being FinSequence such that
A1: fp = (fs1 ^ <*(fp . a)*>) ^ fs2 and
len fs1 = a - 1 and
len fs2 = (len fp) - a by Lm10;
per cases ( fp . a <> 0 or fp . a = 0 ) ;
suppose A2: fp . a <> 0 ; :: thesis: (Product fp) / (fp . a) is Element of NAT
reconsider fs2 = fs2 as FinSequence of NAT by A1, FINSEQ_1:36;
fs1 ^ <*(fp . a)*> is FinSequence of NAT by A1, FINSEQ_1:36;
then reconsider fs1 = fs1 as FinSequence of NAT by FINSEQ_1:36;
Product fp = (Product (fs1 ^ <*(fp . a)*>)) * (Product fs2) by A1, RVSUM_1:97
.= ((fp . a) * (Product fs1)) * (Product fs2) by RVSUM_1:96
.= (fp . a) * ((Product fs1) * (Product fs2)) ;
hence (Product fp) / (fp . a) is Element of NAT by A2, XCMPLX_1:89; :: thesis: verum
end;
suppose A3: fp . a = 0 ; :: thesis: (Product fp) / (fp . a) is Element of NAT
(Product fp) / (fp . a) = (Product fp) * ((fp . a) ") by XCMPLX_0:def 9
.= (Product fp) * 0 by A3
.= 0 ;
hence (Product fp) / (fp . a) is Element of NAT ; :: thesis: verum
end;
end;