let V be RealLinearSpace; :: thesis: ( ex p, q being VECTOR of st
for w being VECTOR of ex a, b being Real st (a * p) + (b * q) = w implies for a, b, c, d being Element of st not a,b // c,d & not a,b // d,c holds
ex t being Element of 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 st
for w being VECTOR of ex a, b being Real st (a * p) + (b * q) = w ; :: thesis: for a, b, c, d being Element of st not a,b // c,d & not a,b // d,c holds
ex t being Element of 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 ; :: thesis: ( not a,b // c,d & not a,b // d,c implies ex t being Element of st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) )
reconsider a' = a, b' = b, c' = c, d' = d as Element of ;
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 st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )
then ( not a',b' // c',d' & not a',b' // d',c' ) by Th33;
then consider t' being VECTOR of such that
A2: ( a',b' // a',t' or a',b' // t',a' ) and
A3: ( c',d' // c',t' or c',d' // t',c' ) by A1, Th31;
reconsider t = t' as Element of ;
( [[c,d],[c,t]] in the CONGR of (OASpace V) or [[c,d],[t,c]] in the CONGR of (OASpace V) ) by A3, Th33;
then A4: ( c,d // c,t or c,d // t,c ) by Def2;
( [[a,b],[a,t]] in the CONGR of (OASpace V) or [[a,b],[t,a]] in the CONGR of (OASpace V) ) by A2, Th33;
then ( a,b // a,t or a,b // t,a ) by Def2;
hence ex t being Element of st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) by A4; :: thesis: verum