now :: thesis: for o being object st o in { (p . i) where i is Element of NAT : p . i <> 0. F } holds
o in the carrier of F

let o be object ; :: thesis: ( o in { (p . i) where i is Element of NAT : p . i <> 0. F } implies o in the carrier of F )
assume o in { (p . i) where i is Element of NAT : p . i <> 0. F } ; :: thesis: o in the carrier of F
then consider i being Element of NAT such that
H: ( o = p . i & p . i <> 0. F ) ;
thus o in the carrier of F by H; :: thesis: verum

end;

then { (p . i) where i is Element of NAT : p . i <> 0. F } c= the carrier of F ;
hence { (p . i) where i is Element of NAT : p . i <> 0. F } is Subset of F ; :: thesis: verum