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 ( A // q * A & A // a * A ) by Def3;

then A2: a * A // q * A by AFF_1:44;

A3: q * A is being_line by A1, Th27;

then A4: a in a * (q * A) by Def3;

q * A // a * (q * A) by A3, Def3;

then A5: a * A // a * (q * A) by A2, AFF_1:44;

a in a * A by A1, Def3;

hence a * A = a * (q * A) by A4, A5, AFF_1:45; :: thesis: verum

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 ( A // q * A & A // a * A ) by Def3;

then A2: a * A // q * A by AFF_1:44;

A3: q * A is being_line by A1, Th27;

then A4: a in a * (q * A) by Def3;

q * A // a * (q * A) by A3, Def3;

then A5: a * A // a * (q * A) by A2, AFF_1:44;

a in a * A by A1, Def3;

hence a * A = a * (q * A) by A4, A5, AFF_1:45; :: thesis: verum