let X be set ; :: thesis: for a, b being Element of Z_2

for x, y being Element of (bspace X)

for c, d being Subset of X st x = c & y = d holds

( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

let a, b be Element of Z_2; :: thesis: for x, y being Element of (bspace X)

for c, d being Subset of X st x = c & y = d holds

( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

let x, y be Element of (bspace X); :: thesis: for c, d being Subset of X st x = c & y = d holds

( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

let c, d be Subset of X; :: thesis: ( x = c & y = d implies ( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) ) )

assume that

A1: x = c and

A2: y = d ; :: thesis: ( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

( a * x = a \*\ c & b * y = b \*\ d ) by A1, A2, Def6;

hence (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) by Def5; :: thesis: ( a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

x + y = c \+\ d by A1, A2, Def5;

hence a * (x + y) = a \*\ (c \+\ d) by Def6; :: thesis: ( (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

thus (a + b) * x = (a + b) \*\ c by A1, Def6; :: thesis: ( (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

thus (a * b) * x = (a * b) \*\ c by A1, Def6; :: thesis: a * (b * x) = a \*\ (b \*\ c)

b * x = b \*\ c by A1, Def6;

hence a * (b * x) = a \*\ (b \*\ c) by Def6; :: thesis: verum

for x, y being Element of (bspace X)

for c, d being Subset of X st x = c & y = d holds

( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

let a, b be Element of Z_2; :: thesis: for x, y being Element of (bspace X)

for c, d being Subset of X st x = c & y = d holds

( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

let x, y be Element of (bspace X); :: thesis: for c, d being Subset of X st x = c & y = d holds

( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

let c, d be Subset of X; :: thesis: ( x = c & y = d implies ( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) ) )

assume that

A1: x = c and

A2: y = d ; :: thesis: ( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

( a * x = a \*\ c & b * y = b \*\ d ) by A1, A2, Def6;

hence (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) by Def5; :: thesis: ( a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

x + y = c \+\ d by A1, A2, Def5;

hence a * (x + y) = a \*\ (c \+\ d) by Def6; :: thesis: ( (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

thus (a + b) * x = (a + b) \*\ c by A1, Def6; :: thesis: ( (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )

thus (a * b) * x = (a * b) \*\ c by A1, Def6; :: thesis: a * (b * x) = a \*\ (b \*\ c)

b * x = b \*\ c by A1, Def6;

hence a * (b * x) = a \*\ (b \*\ c) by Def6; :: thesis: verum