let f1, f2 be FinSequence; :: thesis: f1 c= f1 ^ f2
A1: for x being object st x in dom f1 holds
f1 . x = (f1 ^ f2) . x by FINSEQ_1:def 7;
dom f1 c= dom (f1 ^ f2) by FINSEQ_1:26;
hence f1 c= f1 ^ f2 by A1, GRFUNC_1:2; :: thesis: verum