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