let f be Sequence; :: thesis: f ^ {} = f
reconsider E = {} as Sequence ;
dom E = 0 ;
then A1: ( dom (f ^ {}) = (dom f) +^ 0 & (dom f) +^ 0 = dom f ) by ORDINAL2:27, ORDINAL4:def 1;
for x being object st x in dom f holds
f . x = (f ^ E) . x by ORDINAL4:def 1;
hence f ^ {} = f by A1, FUNCT_1:2; :: thesis: verum