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₁[ set ] means ex f being FinSequence of NAT st
( f = $1 & ( ( for a being Nat st a in dom f holds
(f . a) gcd d = 1 ) implies (Product f) gcd d = 1 ) );

A1: now :: thesis: for fp being FinSequence of NAT
for a being Element of NAT st S₁[fp] holds
S₁[fp ^ <*a*>]

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*>;
take fp ^ <*a*> ; :: thesis: ( fp ^ <*a*> = fp ^ <*a*> & ( ( for a being Nat st a in dom (fp ^ <*a*>) holds
((fp ^ <*a*>) . a) gcd d = 1 ) implies (Product (fp ^ <*a*>)) gcd d = 1 ) )
thus fp ^ <*a*> = fp ^ <*a*> ; :: thesis: ( ( for a being Nat st a in dom (fp ^ <*a*>) holds
((fp ^ <*a*>) . a) gcd d = 1 ) implies (Product (fp ^ <*a*>)) gcd d = 1 )
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:26;
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:16;
then A7: a gcd d = 1 by FINSEQ_1:42;
Product (fp ^ <*a*>) = (Product fp) * a by RVSUM_1:96;
hence (Product (fp ^ <*a*>)) gcd d = 1 by A2, A5, A7, Th6; :: thesis: verum

end;

end;

A8: S₁[ <*> NAT]

proof

take <*> NAT ; :: thesis: ( <*> NAT = <*> NAT & ( ( for a being Nat st a in dom (<*> NAT) holds
((<*> NAT) . a) gcd d = 1 ) implies (Product (<*> NAT)) gcd d = 1 ) )
thus ( <*> NAT = <*> NAT & ( ( for a being Nat st a in dom (<*> NAT) holds
((<*> NAT) . a) gcd d = 1 ) implies (Product (<*> NAT)) gcd d = 1 ) ) by NEWTON:51, RVSUM_1:94; :: thesis: verum

end;

for fp being FinSequence of NAT holds S₁[fp] from FINSEQ_2:sch 2(A8, A1);
then ex f being FinSequence of NAT st
( f = fp & ( ( for a being Nat st a in dom f holds
(f . a) gcd d = 1 ) implies (Product f) gcd d = 1 ) ) ;
hence ( ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) implies (Product fp) gcd d = 1 ) ; :: thesis: verum