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

for A, X being Subset of AS st A is being_line & X is being_plane & A '||' X holds

a * A c= a + X

let a be Element of AS; :: thesis: for A, X being Subset of AS st A is being_line & X is being_plane & A '||' X holds

a * A c= a + X

let A, X be Subset of AS; :: thesis: ( A is being_line & X is being_plane & A '||' X implies a * A c= a + X )

assume that

A1: A is being_line and

A2: X is being_plane and

A3: A '||' X ; :: thesis: a * A c= a + X

A4: ( X '||' a + X & a in a + X ) by A2, Def6;

consider N being Subset of AS such that

A5: N c= X and

A6: ( A // N or N // A ) by A1, A2, A3, Th41;

( a * A = a * N & N is being_line ) by A6, Th32, AFF_1:36;

hence a * A c= a + X by A5, A4; :: thesis: verum

for A, X being Subset of AS st A is being_line & X is being_plane & A '||' X holds

a * A c= a + X

let a be Element of AS; :: thesis: for A, X being Subset of AS st A is being_line & X is being_plane & A '||' X holds

a * A c= a + X

let A, X be Subset of AS; :: thesis: ( A is being_line & X is being_plane & A '||' X implies a * A c= a + X )

assume that

A1: A is being_line and

A2: X is being_plane and

A3: A '||' X ; :: thesis: a * A c= a + X

A4: ( X '||' a + X & a in a + X ) by A2, Def6;

consider N being Subset of AS such that

A5: N c= X and

A6: ( A // N or N // A ) by A1, A2, A3, Th41;

( a * A = a * N & N is being_line ) by A6, Th32, AFF_1:36;

hence a * A c= a + X by A5, A4; :: thesis: verum