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

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