let a be real number ; :: thesis: for G being FinSequence of REAL holds dom G = dom (a * G)
let G be FinSequence of REAL ; :: thesis: dom G = dom (a * G)
len (a * G) = len G by Th6;
hence dom G = dom (a * G) by FINSEQ_3:31; :: thesis: verum