consider V being RealLinearSpace such that

A1: ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) by FUNCSDOM:23;

reconsider X = OASpace V as OAffinSpace by A1, ANALOAF:26;

take X ; :: thesis: ( X is Pappian & X is Desarguesian & X is Moufangian & X is translation )

set AS = Lambda X;

A2: ( Lambda X is Moufangian & Lambda X is translational ) by Th16, Th17;

( Lambda X is Pappian & Lambda X is Desarguesian ) by Th9, Th11, Th13;

hence ( X is Pappian & X is Desarguesian & X is Moufangian & X is translation ) by A2; :: thesis: verum

A1: ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) by FUNCSDOM:23;

reconsider X = OASpace V as OAffinSpace by A1, ANALOAF:26;

take X ; :: thesis: ( X is Pappian & X is Desarguesian & X is Moufangian & X is translation )

set AS = Lambda X;

A2: ( Lambda X is Moufangian & Lambda X is translational ) by Th16, Th17;

( Lambda X is Pappian & Lambda X is Desarguesian ) by Th9, Th11, Th13;

hence ( X is Pappian & X is Desarguesian & X is Moufangian & X is translation ) by A2; :: thesis: verum