let p, q be XFinSequence; :: thesis: p c= p ^ q
A1: dom p c= dom (p ^ q) by Th19;
for x being object st x in dom p holds
(p ^ q) . x = p . x by Def3;
hence p c= p ^ q by A1, GRFUNC_1:2; :: thesis: verum