set g = (F2 _E) * (F1 _E);
set f = (F2 _V) * (F1 _V);
let e, v, w be object ; :: according to GLIB_010:def 15 :: thesis: ( e in dom ((F2 * F1) _E) & v in dom ((F2 * F1) _V) & w in dom ((F2 * F1) _V) & ((F2 * F1) _E) . e Joins ((F2 * F1) _V) . v,((F2 * F1) _V) . w,G3 implies e Joins v,w,G1 )
assume A1: ( e in dom ((F2 * F1) _E) & v in dom ((F2 * F1) _V) & w in dom ((F2 * F1) _V) ) ; :: thesis: ( not ((F2 * F1) _E) . e Joins ((F2 * F1) _V) . v,((F2 * F1) _V) . w,G3 or e Joins v,w,G1 )
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 Joins v,w,G1 iff (F1 _E) . e Joins (F1 _V) . v,(F1 _V) . w,G2 ) by A2, A3, Th15;
then A4: ( e Joins v,w,G1 iff (F2 _E) . ((F1 _E) . e) Joins (F2 _V) . ((F1 _V) . v),(F2 _V) . ((F1 _V) . w),G3 ) by A2, A3, Th15;
( (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 ((F2 * F1) _E) . e Joins ((F2 * F1) _V) . v,((F2 * F1) _V) . w,G3 or e Joins v,w,G1 ) by A1, A4, FUNCT_1:12; :: thesis: verum