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) )
thus (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) :: 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) )

proof

A3: a * x = a \*\ c by A1, Def6;
b * y = b \*\ d by A2, Def6;
hence (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) by A3, Def5; :: thesis: verum

end;

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

proof

A4: x + y = c \+\ d by A1, A2, Def5;
thus a * (x + y) = a \*\ (c \+\ d) by A4, Def6; :: thesis: verum

end;

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)
thus a * (b * x) = a \*\ (b \*\ c) :: thesis: verum

proof

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

end;