let AS be AffinSpace; :: thesis: for a being Element of AS

for K, M being Subset of AS st K // M holds

a * K = a * M

let a be Element of AS; :: thesis: for K, M being Subset of AS st K // M holds

a * K = a * M

let K, M be Subset of AS; :: thesis: ( K // M implies a * K = a * M )

assume A1: K // M ; :: thesis: a * K = a * M

then A2: K is being_line by AFF_1:36;

then K // a * K by Def3;

then A3: a * K // M by A1, AFF_1:44;

A4: M is being_line by A1, AFF_1:36;

then A5: a in a * M by Def3;

M // a * M by A4, Def3;

then A6: a * K // a * M by A3, AFF_1:44;

a in a * K by A2, Def3;

hence a * K = a * M by A5, A6, AFF_1:45; :: thesis: verum

for K, M being Subset of AS st K // M holds

a * K = a * M

let a be Element of AS; :: thesis: for K, M being Subset of AS st K // M holds

a * K = a * M

let K, M be Subset of AS; :: thesis: ( K // M implies a * K = a * M )

assume A1: K // M ; :: thesis: a * K = a * M

then A2: K is being_line by AFF_1:36;

then K // a * K by Def3;

then A3: a * K // M by A1, AFF_1:44;

A4: M is being_line by A1, AFF_1:36;

then A5: a in a * M by Def3;

M // a * M by A4, Def3;

then A6: a * K // a * M by A3, AFF_1:44;

a in a * K by A2, Def3;

hence a * K = a * M by A5, A6, AFF_1:45; :: thesis: verum