let x, y be object ; FUNCT_1:def 4 ( not x in dom the Sorts of A or not y in dom the Sorts of A or not the Sorts of A . x = the Sorts of A . y or x = y )
assume that
A1:
x in dom the Sorts of A
and
A2:
y in dom the Sorts of A
; ( not the Sorts of A . x = the Sorts of A . y or x = y )
reconsider a = x, b = y as SortSymbol of S by A1, A2;
assume that
A3:
the Sorts of A . x = the Sorts of A . y
and
A4:
x <> y
; contradiction
the Sorts of A is disjoint_valued
by MSAFREE1:def 2;
then
the Sorts of A . a misses the Sorts of A . b
by A4, PROB_2:def 2;
hence
contradiction
by A3; verum