let e9, v, w be object ; :: according to GLIB_010:def 16 :: thesis: ( v in dom ((F2 * F1) _V) & w in dom ((F2 * F1) _V) & e9 Joins ((F2 * F1) _V) . v,((F2 * F1) _V) . w,G3 implies ex e being object st
( e Joins v,w,G1 & e in dom ((F2 * F1) _E) & ((F2 * F1) _E) . e = e9 ) )
assume A1: ( v in dom ((F2 * F1) _V) & w in dom ((F2 * F1) _V) & e9 Joins ((F2 * F1) _V) . v,((F2 * F1) _V) . w,G3 ) ; :: thesis: ex e being object st
( e Joins v,w,G1 & e in dom ((F2 * F1) _E) & ((F2 * F1) _E) . e = e9 )
then A2: ( 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 FUNCT_1:11;
then ( ((F2 * F1) _V) . v = (F2 _V) . ((F1 _V) . v) & ((F2 * F1) _V) . w = (F2 _V) . ((F1 _V) . w) ) by FUNCT_1:13;
then consider e8 being object such that
A3: ( e8 Joins (F1 _V) . v,(F1 _V) . w,G2 & e8 in dom (F2 _E) & (F2 _E) . e8 = e9 ) by A1, A2, Def16;
consider e being object such that
A4: ( e Joins v,w,G1 & e in dom (F1 _E) & (F1 _E) . e = e8 ) by A2, A3, Def16;
take e ; :: thesis: ( e Joins v,w,G1 & e in dom ((F2 * F1) _E) & ((F2 * F1) _E) . e = e9 )
thus e Joins v,w,G1 by A4; :: thesis: ( e in dom ((F2 * F1) _E) & ((F2 * F1) _E) . e = e9 )
thus e in dom ((F2 * F1) _E) by A3, A4, FUNCT_1:11; :: thesis: ((F2 * F1) _E) . e = e9
hence ((F2 * F1) _E) . e = e9 by A3, A4, FUNCT_1:12; :: thesis: verum