let f1, f2 be Sequence; :: thesis: f1 c= f1 ^ f2
dom (f1 ^ f2) = (dom f1) +^ (dom f2) by ORDINAL4:def 1;
then A1: dom f1 c= dom (f1 ^ f2) by ORDINAL3:24;
for x being object st x in dom f1 holds
f1 . x = (f1 ^ f2) . x by ORDINAL4:def 1;
hence f1 c= f1 ^ f2 by A1, GRFUNC_1:2; :: thesis: verum