let A, B be complex-membered set ; :: thesis: for a, b being Complex st a in A & b in B holds
a / b in A /// B
let a, b be Complex; :: thesis: ( a in A & b in B implies a / b in A /// B )
A /// B = { (c1 / c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } by Th115;
hence ( a in A & b in B implies a / b in A /// B ) ; :: thesis: verum