let n be Nat; :: thesis:
let r be FinSequence of F_Rat; :: thesis:
assume len r = n ; :: thesis:
then consider K being Integer such that
P1: ( K <> 0 & ( for i being Nat st i in Seg n holds
K * (r /. i) in INT ) ) by LMThGM231;
defpred S₁[ Nat, object ] means $2 = K * (r /. $1);
Z510: for i being Nat st i in Seg n holds
ex x being Element of the carrier of INT.Ring st S₁[i,x]

let i be Nat; :: thesis:
assume i in Seg n ; :: thesis:
then reconsider x = K * (r /. i) as Element of INT.Ring by P1;
take x ; :: thesis:
thus S₁[i,x] ; :: thesis:

end;

consider Kr being FinSequence of the carrier of INT.Ring such that
Z511: ( dom Kr = Seg n & ( for k being Nat st k in Seg n holds
S₁[k,Kr . k] ) ) from FINSEQ_1:sch 5(Z510);
take K ; :: thesis:
take Kr ; :: thesis:
thus K <> 0 by P1; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence len Kr = n by Z511, FINSEQ_1:def 3; :: thesis:
thus for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) by Z511; :: thesis: