let X be non empty set ; :: thesis: for l being Linear_Combination of bspace X
for x being Element of (bspace X) st x in Carrier l holds
l . x = 1_ Z_2
let l be Linear_Combination of bspace X; :: thesis: for x being Element of (bspace X) st x in Carrier l holds
l . x = 1_ Z_2
let x be Element of (bspace X); :: thesis: ( x in Carrier l implies l . x = 1_ Z_2 )
assume x in Carrier l ; :: thesis: l . x = 1_ Z_2
then l . x <> 0. Z_2 by VECTSP_6:2;
hence l . x = 1_ Z_2 by Th5, Th6, CARD_1:50, TARSKI:def 2; :: thesis: verum