let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in K49((0Functional V)) or not y in K49((0Functional V)) or (0Functional V) . x = (0Functional V) . y )
set f = 0Functional V;
assume ( x in dom (0Functional V) & y in dom (0Functional V) ) ; :: thesis: (0Functional V) . x = (0Functional V) . y
then reconsider v = x, w = y as Vector of V ;
thus (0Functional V) . x = (0Functional V) . v
.= 0. K by HAHNBAN1:14
.= (0Functional V) . w by HAHNBAN1:14
.= (0Functional V) . y ; :: thesis: verum