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

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