let n be Nat; :: thesis: ex f being integer-valued AP-like XFinSequence st
( dom f >= n & f is with_all_coprime_terms )
set f = ArProg (((n !) + 1),(n !));
reconsider ff = (ArProg (((n !) + 1),(n !))) | n as integer-valued XFinSequence by RestrictedXFin;
SS: for k being Nat holds (ArProg (((n !) + 1),(n !))) . k = ((n !) * (k + 1)) + 1

proof

let k be Nat; :: thesis: (ArProg (((n !) + 1),(n !))) . k = ((n !) * (k + 1)) + 1
(ArProg (((n !) + 1),(n !))) . k = ((n !) + 1) + ((n !) * k) by ArDefNth
.= ((n !) * (k + 1)) + 1 ;
hence (ArProg (((n !) + 1),(n !))) . k = ((n !) * (k + 1)) + 1 ; :: thesis: verum

end;

S0: for k being Nat st k + 1 <= n holds
ff . k = ((n !) * (k + 1)) + 1

proof

let k be Nat; :: thesis: ( k + 1 <= n implies ff . k = ((n !) * (k + 1)) + 1 )
assume k + 1 <= n ; :: thesis: ff . k = ((n !) * (k + 1)) + 1
then k < n by NAT_1:13;
then k in Segm n by NAT_1:44;
then ff . k = (ArProg (((n !) + 1),(n !))) . k by FUNCT_1:49;
hence ff . k = ((n !) * (k + 1)) + 1 by SS; :: thesis: verum

end;

dom (ArProg (((n !) + 1),(n !))) = NAT by FUNCT_2:def 1;
then t2: dom ((ArProg (((n !) + 1),(n !))) | (Segm n)) = Segm n ;
for i, j being Nat st i in dom ff & j in dom ff & i <> j holds
ff . i,ff . j are_coprime

proof

let i, j be Nat; :: thesis: ( i in dom ff & j in dom ff & i <> j implies ff . i,ff . j are_coprime )
assume S1: ( i in dom ff & j in dom ff & i <> j ) ; :: thesis: ff . i,ff . j are_coprime
then S2: i + 1 <> j + 1 ;
S6: ( 1 <= i + 1 & 1 <= j + 1 ) by NAT_1:12;
( i < n & j < n ) by NAT_1:44, S1, t2;
then S4: ( i + 1 <= n & j + 1 <= n ) by NAT_1:13;
then ( ff . i = ((n !) * (i + 1)) + 1 & ff . j = ((n !) * (j + 1)) + 1 ) by S0;
hence ff . i,ff . j are_coprime by S4, S6, S2, LemmaFor52; :: thesis: verum

end;

then ff is with_all_coprime_terms ;
hence ex f being integer-valued AP-like XFinSequence st
( dom f >= n & f is with_all_coprime_terms ) by t2; :: thesis: verum