take 0. F_Complex ; :: thesis: 0. F_Complex is F_Real -membered
thus 0. F_Complex is F_Real -membered ; :: thesis: verum