let X, Y be RealLinearSpace; ((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; verum