let x, y be object ; :: thesis: for X being set
for z being object st z <> x holds
((X --> 0) +* (x,y)) . z = 0
let X be set ; :: thesis: for z being object st z <> x holds
((X --> 0) +* (x,y)) . z = 0
let z be object ; :: thesis: ( z <> x implies ((X --> 0) +* (x,y)) . z = 0 )
assume A1: z <> x ; :: thesis: ((X --> 0) +* (x,y)) . z = 0
A2: dom (X --> 0) = X by FUNCOP_1:13;

per cases ( z in X or not z in X ) ;

suppose A3: z in X ; :: thesis: ((X --> 0) +* (x,y)) . z = 0

((X --> 0) +* (x,y)) . z = (X --> 0) . z by A1, FUNCT_7:32
.= 0 by A3, FUNCOP_1:7 ;
hence ((X --> 0) +* (x,y)) . z = 0 ; :: thesis: verum

end;

suppose A4: not z in X ; :: thesis: ((X --> 0) +* (x,y)) . z = 0

((X --> 0) +* (x,y)) . z = (X --> 0) . z by A1, FUNCT_7:32
.= 0 by A2, A4, FUNCT_1:def 2 ;
hence ((X --> 0) +* (x,y)) . z = 0 ; :: thesis: verum

end;

end;