let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 (p ^ q) or (p ^ q) . x is set )
assume A1: x in dom (p ^ q) ; :: thesis: (p ^ q) . x is set
then reconsider i = x as Nat ;

per cases ( i in dom p or not i in dom p ) ;

suppose i in dom p ; :: thesis: (p ^ q) . x is set

then p . i = (p ^ q) . i by FINSEQ_1:def 7;
hence (p ^ q) . x is set ; :: thesis: verum

end;

suppose not i in dom p ; :: thesis: (p ^ q) . x is set

then consider j being Nat such that
A2: ( j in dom q & i = (len p) + j ) by A1, FINSEQ_1:25;
q . j = (p ^ q) . i by A2, FINSEQ_1:def 7;
hence (p ^ q) . x is set ; :: thesis: verum

end;

end;