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; :: thesis: verum