let B be array; :: thesis: ( B = Swap (A,x,y) implies B is real-valued )
assume A1: B = Swap (A,x,y) ; :: thesis: B is real-valued
let z be object ; :: according to VALUED_0:def 9 :: thesis: ( not z in proj1 B or not B . z is V75() )
assume z in dom B ; :: thesis: B . z is V75()
then A2: ( z in dom A & ( x = z or x <> z ) & ( y = z or y <> z ) ) by A1, FUNCT_7:99;
( ( not x in dom A or not y in dom A ) implies B = A ) by A1, FUNCT_7:def 12;
then ( B . z = A . y or B . z = A . x or B . z = A . z ) by A1, A2, Th29, Th31, Th33;
hence B . z is V75() ; :: thesis: verum