let N be Element of NAT ; :: thesis: for r, q being Real
for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq)
let r, q be Real; :: thesis: for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq)
let seq be Real_Sequence of N; :: thesis: (r * q) * seq = r * (q * seq)

now

let n be Element of NAT ; :: thesis: ((r * q) * seq) . n = (r * (q * seq)) . n
thus ((r * q) * seq) . n = (r * q) * (seq . n) by Def3
.= r * (q * (seq . n)) by EUCLID:34
.= r * ((q * seq) . n) by Def3
.= (r * (q * seq)) . n by Def3 ; :: thesis: verum

end;

hence (r * q) * seq = r * (q * seq) by FUNCT_2:113; :: thesis: verum