now :: thesis: for f, g being object st f in the carrier of (product F) & g in the carrier of (product F) holds
f = g

let f, g be object ; :: thesis: ( f in the carrier of (product F) & g in the carrier of (product F) implies f = g )
assume ( f in the carrier of (product F) & g in the carrier of (product F) ) ; :: thesis: f = g
then ( f in product (Carrier F) & g in product (Carrier F) ) by Def2;
then ( f = {} & g = {} ) ;
hence f = g ; :: thesis: verum

end;

hence product F is trivial by ZFMISC_1:def 10; :: thesis: verum