let G1, G2, G3 be _Graph; :: thesis: for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is directed & g is directed holds
g * f is directed
let f be PVertexMapping of G1,G2; :: thesis: for g being PVertexMapping of G2,G3 st f is directed & g is directed holds
g * f is directed
let g be PVertexMapping of G2,G3; :: thesis: ( f is directed & g is directed implies g * f is directed )
assume A1: ( f is directed & g is directed ) ; :: thesis: g * f is directed
now :: thesis: for v, w, e9 being object st v in dom (g * f) & w in dom (g * f) & e9 DJoins v,w,G1 holds
ex e being object st e DJoins (g * f) . v,(g * f) . w,G3
let v, w, e9 be object ; :: thesis: ( v in dom (g * f) & w in dom (g * f) & e9 DJoins v,w,G1 implies ex e being object st e DJoins (g * f) . v,(g * f) . w,G3 )
assume A2: ( v in dom (g * f) & w in dom (g * f) & e9 DJoins v,w,G1 ) ; :: thesis: ex e being object st e DJoins (g * f) . v,(g * f) . w,G3
then ( v in dom f & w in dom f ) by FUNCT_1:11;
then consider e8 being object such that
A3: e8 DJoins f . v,f . w,G2 by A1, A2;
( f . v in dom g & f . w in dom g ) by A2, FUNCT_1:11;
then consider e being object such that
A4: e DJoins g . (f . v),g . (f . w),G3 by A1, A3;
take e = e; :: thesis: e DJoins (g * f) . v,(g * f) . w,G3
e DJoins (g * f) . v,g . (f . w),G3 by A2, A4, FUNCT_1:12;
hence e DJoins (g * f) . v,(g * f) . w,G3 by A2, FUNCT_1:12; :: thesis: verum
end;
hence g * f is directed ; :: thesis: verum