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