consider a1, a2 being Ordinal such that
A1: dom A = a1 \ a2 by Def1;
take a1 ; :: according to EXCHSORT:def 1 :: thesis: ex b being Ordinal st proj1 (Swap (A,x,y)) = a1 \ b
take a2 ; :: thesis: proj1 (Swap (A,x,y)) = a1 \ a2
thus proj1 (Swap (A,x,y)) = a1 \ a2 by A1, FUNCT_7:99; :: thesis: verum