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

proof

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

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

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

end;

end;

end;

hence p ^ q is Cycle-like ; :: thesis: verum