let n be Nat; :: thesis: for r being FinSequence of F_Rat st len r = n holds
ex K being Integer ex Kr being FinSequence of INT.Ring st
( K <> 0 & len Kr = n & ( for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) ) )
let r be FinSequence of F_Rat; :: thesis: ( len r = n implies ex K being Integer ex Kr being FinSequence of INT.Ring st
( K <> 0 & len Kr = n & ( for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) ) ) )
assume len r = n ; :: thesis: ex K being Integer ex Kr being FinSequence of INT.Ring st
( K <> 0 & len Kr = n & ( for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) ) )
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]

proof

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

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: ex Kr being FinSequence of INT.Ring st
( K <> 0 & len Kr = n & ( for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) ) )
take Kr ; :: thesis: ( K <> 0 & len Kr = n & ( for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) ) )
thus K <> 0 by P1; :: thesis: ( len Kr = n & ( for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) ) )
n is Element of NAT by ORDINAL1:def 12;
hence len Kr = n by Z511, FINSEQ_1:def 3; :: thesis: for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i)
thus for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) by Z511; :: thesis: verum