A1:
dom (f +* (a,x)) = dom f
by FUNCT_7:30;
then
( ( for b being Ordinal st b in dom (f +* (a,x)) holds
( i in dom f & i c= b ) ) & ex c, b being Ordinal st dom (f +* (a,x)) = c \ b )
by EXCHSORT:def 1, EXCHSORT:def 2;
hence
( f +* (a,x) is i -based & f +* (a,x) is finite & f +* (a,x) is segmental )
by A1, FINSET_1:10, EXCHSORT:def 1, EXCHSORT:def 2; verum