let AS be AffinSpace; :: thesis: for a, q being Element of AS
for A being Subset of AS st A is being_line holds
a * A = a * (q * A)
let a, q be Element of AS; :: thesis: for A being Subset of AS st A is being_line holds
a * A = a * (q * A)
let A be Subset of AS; :: thesis: ( A is being_line implies a * A = a * (q * A) )
assume A1: A is being_line ; :: thesis: a * A = a * (q * A)
then q * A is being_line by Th27;
then A2: ( A // q * A & A // a * A & q * A // a * (q * A) & a in a * A & a in a * (q * A) ) by A1, Def3;
then a * A // q * A by AFF_1:58;
then a * A // a * (q * A) by A2, AFF_1:58;
hence a * A = a * (q * A) by A2, AFF_1:59; :: thesis: verum