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

proof

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

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

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

end;

end;

end;

hence p ^ q is non-trivial by GLIB_000:def 61; :: thesis: verum