let fp be FinSequence of NAT ; :: thesis: for d being Nat st ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) holds
(Product fp) gcd d = 1
let d be Nat; :: thesis: ( ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) implies (Product fp) gcd d = 1 )
defpred S₁[ FinSequence of NAT ] means ( ( for a being Nat st a in dom $1 holds
($1 . a) gcd d = 1 ) implies (Product $1) gcd d = 1 );

A1: now

let fp be FinSequence of NAT ; :: thesis: for a being Element of NAT st S₁[fp] holds
S₁[fp ^ <*a*>]
let a be Element of NAT ; :: thesis: ( S₁[fp] implies S₁[fp ^ <*a*>] )
assume A2: S₁[fp] ; :: thesis: S₁[fp ^ <*a*>]
thus S₁[fp ^ <*a*>] :: thesis: verum

proof

set fp1 = fp ^ <*a*>;
assume A3: for b being Nat st b in dom (fp ^ <*a*>) holds
((fp ^ <*a*>) . b) gcd d = 1 ; :: thesis: (Product (fp ^ <*a*>)) gcd d = 1
A4: dom fp c= dom (fp ^ <*a*>) by FINSEQ_1:39;
A5: for b being Nat st b in dom fp holds
(fp . b) gcd d = 1

proof

let b be Nat; :: thesis: ( b in dom fp implies (fp . b) gcd d = 1 )
assume A6: b in dom fp ; :: thesis: (fp . b) gcd d = 1
then ((fp ^ <*a*>) . b) gcd d = 1 by A3, A4;
hence (fp . b) gcd d = 1 by A6, FINSEQ_1:def 7; :: thesis: verum

end;

len (fp ^ <*a*>) in dom (fp ^ <*a*>) by FINSEQ_5:6;
then ( len (fp ^ <*a*>) = (len fp) + 1 & ((fp ^ <*a*>) . (len (fp ^ <*a*>))) gcd d = 1 ) by A3, FINSEQ_2:19;
then A7: a gcd d = 1 by FINSEQ_1:59;
Product (fp ^ <*a*>) = (Product fp) * a by RVSUM_1:126;
hence (Product (fp ^ <*a*>)) gcd d = 1 by A2, A5, A7, Th11; :: thesis: verum

end;

end;

A8: S₁[ <*> NAT ] by NEWTON:64, RVSUM_1:124;
for fp being FinSequence of NAT holds S₁[fp] from FINSEQ_2:sch 2(A8, A1);
hence ( ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) implies (Product fp) gcd d = 1 ) ; :: thesis: verum