now :: thesis: for x being object st x in dom (A ^ B) holds
not (A ^ B) . x is empty

let x be object ; :: thesis: ( x in dom (A ^ B) implies not (A ^ B) . b₁ is empty )
assume A1: x in dom (A ^ B) ; :: thesis: not (A ^ B) . b₁ is empty
then reconsider c = x as Ordinal ;

per cases ( c in dom A or not c in dom A ) ;

suppose A2: c in dom A ; :: thesis: not (A ^ B) . b₁ is empty

then (A ^ B) . c = A . c by ORDINAL4:def 1;
hence not (A ^ B) . x is empty by A2, FUNCT_1:def 9; :: thesis: verum

end;

suppose not c in dom A ; :: thesis: not (A ^ B) . b₁ is empty

then consider d being Ordinal such that
A3: c = (dom A) +^ d by ORDINAL1:16, ORDINAL3:27;
c in (dom A) +^ (dom B) by A1, ORDINAL4:def 1;
then A4: d in dom B by A3, ORDINAL3:22;
then (A ^ B) . ((dom A) +^ d) = B . d by ORDINAL4:def 1;
hence not (A ^ B) . x is empty by A3, A4, FUNCT_1:def 9; :: thesis: verum

end;

end;

end;

hence A ^ B is non-empty by FUNCT_1:def 9; :: thesis: verum