now :: thesis: for o being object st o in h .: T holds
o in the carrier of E2

let o be object ; :: thesis: ( o in h .: T implies o in the carrier of E2 )
assume o in h .: T ; :: thesis: o in the carrier of E2
then consider x being object such that
B: ( x in dom h & x in T & o = h . x ) by FUNCT_1:def 6;
thus o in the carrier of E2 by B, FUNCT_2:5; :: thesis: verum

end;

then h .: T c= the carrier of E2 ;
hence h .: T is Subset of E2 ; :: thesis: verum