let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (StoneH L) or not x2 in dom (StoneH L) or not (StoneH L) . x1 = (StoneH L) . x2 or x1 = x2 )
assume that
A1: x1 in dom (StoneH L) and
A2: x2 in dom (StoneH L) and
A3: (StoneH L) . x1 = (StoneH L) . x2 ; :: thesis: x1 = x2
reconsider a1 = x1, a2 = x2 as Element of L by A1, A2, Def6;
a1 = a2 by A3, Th22;
hence x1 = x2 ; :: thesis: verum