let p, q be XFinSequence; :: thesis: p c= p ^ q
A1: dom p c= dom (p ^ q) by Th24;
for x being set st x in dom p holds
(p ^ q) . x = p . x

proof

let x be set ; :: thesis: ( x in dom p implies (p ^ q) . x = p . x )
assume A2: x in dom p ; :: thesis: (p ^ q) . x = p . x
then reconsider x = x as Nat ;
(p ^ q) . x = p . x by A2, Def4;
hence (p ^ q) . x = p . x ; :: thesis: verum

end;

hence p c= p ^ q by A1, GRFUNC_1:2; :: thesis: verum