let f, g be Function; :: thesis: ( dom f = dom g & f is segmental implies g is segmental )
assume Z0: dom f = dom g ; :: thesis: ( not f is segmental or g is segmental )
given a, b being ordinal number such that Z1: dom f = a \ b ; :: according to EXCHSORT:def 1 :: thesis: g is segmental
take a ; :: according to EXCHSORT:def 1 :: thesis: ex b being ordinal number st proj1 g = a \ b
take b ; :: thesis: proj1 g = a \ b
thus proj1 g = a \ b by Z0, Z1; :: thesis: verum