set g = (F2 _E) * (F1 _E);
set f = (F2 _V) * (F1 _V);
let e, v, w be object ; :: according to GLIB_010:def 14 :: thesis: ( e in dom ((F2 * F1) _E) & v in dom ((F2 * F1) _V) & w in dom ((F2 * F1) _V) & e DJoins v,w,G1 implies ((F2 * F1) _E) . e DJoins ((F2 * F1) _V) . v,((F2 * F1) _V) . w,G3 )
assume A1: ( e in dom ((F2 * F1) _E) & v in dom ((F2 * F1) _V) & w in dom ((F2 * F1) _V) ) ; :: thesis: ( not e DJoins v,w,G1 or ((F2 * F1) _E) . e DJoins ((F2 * F1) _V) . v,((F2 * F1) _V) . w,G3 )
then A2: ( e in dom (F1 _E) & (F1 _E) . e in dom (F2 _E) ) by FUNCT_1:11;
A3: ( v in dom (F1 _V) & (F1 _V) . v in dom (F2 _V) & w in dom (F1 _V) & (F1 _V) . w in dom (F2 _V) ) by A1, FUNCT_1:11;
( e DJoins v,w,G1 implies (F1 _E) . e DJoins (F1 _V) . v,(F1 _V) . w,G2 ) by A2, A3, Def14;
then A4: ( e DJoins v,w,G1 implies (F2 _E) . ((F1 _E) . e) DJoins (F2 _V) . ((F1 _V) . v),(F2 _V) . ((F1 _V) . w),G3 ) by A2, A3, Def14;
( (F2 _V) . ((F1 _V) . v) = ((F2 _V) * (F1 _V)) . v & (F2 _V) . ((F1 _V) . w) = ((F2 _V) * (F1 _V)) . w ) by A1, FUNCT_1:12;
hence ( not e DJoins v,w,G1 or ((F2 * F1) _E) . e DJoins ((F2 * F1) _V) . v,((F2 * F1) _V) . w,G3 ) by A1, A4, FUNCT_1:12; :: thesis: verum