let V be RealLinearSpace; :: thesis: ( ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w implies for a, b, c, d being Element of (OASpace V) st not a,b // c,d & not a,b // d,c holds
ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) )
assume A1: ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w ; :: thesis: for a, b, c, d being Element of (OASpace V) st not a,b // c,d & not a,b // d,c holds
ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )
set S = OASpace V;
let a, b, c, d be Element of (OASpace V); :: thesis: ( not a,b // c,d & not a,b // d,c implies ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of V ;
assume ( not [[a,b],[c,d]] in the CONGR of (OASpace V) & not [[a,b],[d,c]] in the CONGR of (OASpace V) ) ; :: according to ANALOAF:def 2 :: thesis: ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )
then ( not a9,b9 // c9,d9 & not a9,b9 // d9,c9 ) by Th22;
then consider t9 being VECTOR of V such that
A2: ( a9,b9 // a9,t9 or a9,b9 // t9,a9 ) and
A3: ( c9,d9 // c9,t9 or c9,d9 // t9,c9 ) by A1, Th21;
reconsider t = t9 as Element of (OASpace V) ;
( [[c,d],[c,t]] in the CONGR of (OASpace V) or [[c,d],[t,c]] in the CONGR of (OASpace V) ) by A3, Th22;
then A4: ( c,d // c,t or c,d // t,c ) ;
( [[a,b],[a,t]] in the CONGR of (OASpace V) or [[a,b],[t,a]] in the CONGR of (OASpace V) ) by A2, Th22;
then ( a,b // a,t or a,b // t,a ) ;
hence ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) by A4; :: thesis: verum