let AS be AffinSpace; 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; for A being Subset of AS st A is being_line holds
a * A = a * (q * A)
let A be Subset of AS; ( A is being_line implies a * A = a * (q * A) )
assume A1:
A is being_line
; 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; verum