now :: thesis: for x being set st x in dom (p ^ q) holds

(p ^ q) . x is XFinSequence

hence
p ^ q is XFinSequence-yielding
; :: thesis: verum(p ^ q) . x is XFinSequence

let x be set ; :: thesis: ( x in dom (p ^ q) implies (p ^ q) . b_{1} is XFinSequence )

assume A1: x in dom (p ^ q) ; :: thesis: (p ^ q) . b_{1} is XFinSequence

then reconsider x1 = x as Nat ;

end;assume A1: x in dom (p ^ q) ; :: thesis: (p ^ q) . b

then reconsider x1 = x as Nat ;