now :: thesis: for z being object st z in dom (X ^ Y) holds
not (X ^ Y) . z is empty

let z be object ; :: thesis: ( z in dom (X ^ Y) implies not (X ^ Y) . b₁ is empty )
assume A1: z in dom (X ^ Y) ; :: thesis: not (X ^ Y) . b₁ is empty
then reconsider k = z as Element of NAT ;

per cases ( k in dom X or ex n being Nat st
( n in dom Y & k = (len X) + n ) ) by A1, FINSEQ_1:25;

suppose A2: k in dom X ; :: thesis: not (X ^ Y) . b₁ is empty

then X . k = (X ^ Y) . k by FINSEQ_1:def 7;
hence not (X ^ Y) . z is empty by A2; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom Y & k = (len X) + n ) ; :: thesis: not (X ^ Y) . b₁ is empty

then consider n being Nat such that
A3: ( n in dom Y & k = (len X) + n ) ;
Y . n = (X ^ Y) . k by A3, FINSEQ_1:def 7;
hence not (X ^ Y) . z is empty by A3; :: thesis: verum

end;

end;

end;

hence X ^ Y is non-empty by FUNCT_1:def 9; :: thesis: verum