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 S1[ 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 S1[i,x]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex x being Element of the carrier of INT.Ring st S1[i,x] )
assume i in Seg n ; :: thesis: ex x being Element of the carrier of INT.Ring st S1[i,x]
then reconsider x = K * (r /. i) as Element of INT.Ring by P1;
take x ; :: thesis: S1[i,x]
thus S1[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
S1[k,Kr . k] ) ) from 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 ; :: 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