the carrier of F c= the carrier of E by EC_PF_1:def 1;
hence a is Element of E ; :: thesis: verum