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

proof

let x be object ; :: thesis: ( x in dom (p ^ q) implies ex G being _Graph st
( G = (p ^ q) . x & G is acyclic ) )
assume A1: x in dom (p ^ q) ; :: thesis: ex G being _Graph st
( G = (p ^ q) . x & G is acyclic )
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 acyclic )

then ( (p ^ q) . k = p . k & ex G being _Graph st
( p . k = G & G is acyclic ) ) by FINSEQ_1:def 7, GLIB_002:def 13;
hence ex G being _Graph st
( (p ^ q) . x = G & G is acyclic ) ; :: 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 acyclic )

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 acyclic ) ) by A2, FINSEQ_1:def 7, GLIB_002:def 13;
hence ex G being _Graph st
( (p ^ q) . x = G & G is acyclic ) by A2; :: thesis: verum

end;

end;

end;

hence p ^ q is acyclic by GLIB_002:def 13; :: thesis: verum