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_{1}[ 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_{1}[i,x]

Z511: ( dom Kr = Seg n & ( for k being Nat st k in Seg n holds

S_{1}[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

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

Z510: for i being Nat st i in Seg n holds

ex x being Element of the carrier of INT.Ring st S

proof

consider Kr being FinSequence of the carrier of INT.Ring such that
let i be Nat; :: thesis: ( i in Seg n implies ex x being Element of the carrier of INT.Ring st S_{1}[i,x] )

assume i in Seg n ; :: thesis: ex x being Element of the carrier of INT.Ring st S_{1}[i,x]

then reconsider x = K * (r /. i) as Element of INT.Ring by P1;

take x ; :: thesis: S_{1}[i,x]

thus S_{1}[i,x]
; :: thesis: verum

end;assume i in Seg n ; :: thesis: ex x being Element of the carrier of INT.Ring st S

then reconsider x = K * (r /. i) as Element of INT.Ring by P1;

take x ; :: thesis: S

thus S

Z511: ( dom Kr = Seg n & ( for k being Nat st k in Seg n holds

S

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