now :: thesis: for x being object st x in dom (p ^ q) holds
(p ^ q) . x is _Graph

let x be object ; :: thesis: ( x in dom (p ^ q) implies (p ^ q) . b₁ is _Graph )
assume A1: x in dom (p ^ q) ; :: thesis: (p ^ q) . b₁ is _Graph
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: (p ^ q) . b₁ is _Graph

then ( (p ^ q) . k = p . k & p . k is _Graph ) by FINSEQ_1:def 7, GLIB_000:def 53;
hence (p ^ q) . x is _Graph ; :: thesis: verum

end;

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

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

end;

end;

end;

hence p ^ q is Graph-yielding by GLIB_000:def 53; :: thesis: verum