let F1, F2 be finite set ; :: thesis: for E1 being Enumeration of F1
for E2 being Enumeration of F2 st F1 misses F2 holds
E1 ^ E2 is Enumeration of F1 \/ F2
let E1 be Enumeration of F1; :: thesis: for E2 being Enumeration of F2 st F1 misses F2 holds
E1 ^ E2 is Enumeration of F1 \/ F2
let E2 be Enumeration of F2; :: thesis: ( F1 misses F2 implies E1 ^ E2 is Enumeration of F1 \/ F2 )
assume A1: F1 misses F2 ; :: thesis: E1 ^ E2 is Enumeration of F1 \/ F2
( rng E1 = F1 & rng E2 = F2 ) by RLAFFIN3:def 1;
then ( E1 ^ E2 is one-to-one & rng (E1 ^ E2) = F1 \/ F2 ) by A1, FINSEQ_3:91, FINSEQ_1:31;
hence E1 ^ E2 is Enumeration of F1 \/ F2 by RLAFFIN3:def 1; :: thesis: verum