let V be RealLinearSpace; :: thesis: for F1, F2 being Subset-Family of V st F1 is affinely-independent & F2 is affinely-independent holds
F1 \/ F2 is affinely-independent
let F1, F2 be Subset-Family of V; :: thesis: ( F1 is affinely-independent & F2 is affinely-independent implies F1 \/ F2 is affinely-independent )
assume A1: ( F1 is affinely-independent & F2 is affinely-independent ) ; :: thesis: F1 \/ F2 is affinely-independent
let A be Subset of V; :: according to RLAFFIN1:def 5 :: thesis: ( A in F1 \/ F2 implies A is affinely-independent )
assume A in F1 \/ F2 ; :: thesis: A is affinely-independent
then ( A in F1 or A in F2 ) by XBOOLE_0:def 3;
hence A is affinely-independent by A1; :: thesis: verum