let A be complex-membered set ; :: thesis: for a being Complex
for e being set st e in a ++ A holds
ex c being Complex st
( e = a + c & c in A )
let a be Complex; :: thesis: for e being set st e in a ++ A holds
ex c being Complex st
( e = a + c & c in A )
let e be set ; :: thesis: ( e in a ++ A implies ex c being Complex st
( e = a + c & c in A ) )
a ++ A = { (a + c) where c is Complex : c in A } by Th142;
hence ( e in a ++ A implies ex c being Complex st
( e = a + c & c in A ) ) ; :: thesis: verum