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

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