let x be Element of F_Complex; :: thesis: In ((1. F_Complex),(FQ x)) = 1. F_Complex
1. F_Complex = 1. F_Rat by C0SP1:def 3, Th3;
hence In ((1. F_Complex),(FQ x)) = 1. F_Complex by Lm48, SUBSET_1:def 8; :: thesis: verum