let X be non empty set ; :: thesis: for x being Element of X holds (<*> (bspace X)) @ x = <*> Z_2
let x be Element of X; :: thesis: (<*> (bspace X)) @ x = <*> Z_2
set V = bspace X;
set L = (<*> (bspace X)) @ x;
len ((<*> (bspace X)) @ x) = len (<*> (bspace X)) by Def9
.= 0 ;
hence (<*> (bspace X)) @ x = <*> Z_2 ; :: thesis: verum