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 ( K is being_line & M is being_line ) by AFF_1:50;
then A2: ( a in a * K & a in a * M & K // a * K & M // a * M ) by Def3;
then a * K // M by A1, AFF_1:58;
then a * K // a * M by A2, AFF_1:58;
hence a * K = a * M by A2, AFF_1:59; :: thesis: verum