for x being object st x in dom (p ^ q) holds
ex G being _Graph st
( G = (p ^ q) . x & G is connected )

proof

let x be object ; :: thesis: ( x in dom (p ^ q) implies ex G being _Graph st
( G = (p ^ q) . x & G is connected ) )
assume A1: x in dom (p ^ q) ; :: thesis: ex G being _Graph st
( G = (p ^ q) . x & G is connected )
then reconsider k = x as Nat ;

per cases ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A1, FINSEQ_1:25;

suppose k in dom p ; :: thesis: ex G being _Graph st
( G = (p ^ q) . x & G is connected )

then ( (p ^ q) . k = p . k & ex G being _Graph st
( p . k = G & G is connected ) ) by FINSEQ_1:def 7, GLIB_002:def 12;
hence ex G being _Graph st
( (p ^ q) . x = G & G is connected ) ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom q & k = (len p) + n ) ; :: thesis: ex G being _Graph st
( G = (p ^ q) . x & G is connected )

then consider n being Nat such that
A2: ( n in dom q & k = (len p) + n ) ;
( (p ^ q) . ((len p) + n) = q . n & ex G being _Graph st
( q . n = G & G is connected ) ) by A2, FINSEQ_1:def 7, GLIB_002:def 12;
hence ex G being _Graph st
( (p ^ q) . x = G & G is connected ) by A2; :: thesis: verum

end;

end;

end;

hence p ^ q is connected by GLIB_002:def 12; :: thesis: verum