let X, Y be RealNormSpace; :: thesis: ((IsoCPNrSP (X,Y)) ") . (0. (product <*X,Y*>)) = 0. [:X,Y:]
set I = IsoCPNrSP (X,Y);
set J = (IsoCPNrSP (X,Y)) " ;
P0: dom (IsoCPNrSP (X,Y)) = the carrier of [:X,Y:] by FUNCT_2:def 1;
((IsoCPNrSP (X,Y)) ") . (0. (product <*X,Y*>)) = ((IsoCPNrSP (X,Y)) ") . ((IsoCPNrSP (X,Y)) . (0. [:X,Y:])) by ZeZe;
hence ((IsoCPNrSP (X,Y)) ") . (0. (product <*X,Y*>)) = 0. [:X,Y:] by P0, FUNCT_1:34; :: thesis: verum