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