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