let X be set ; :: thesis: for a, b being Element of Z_2
for x, y being Element of ()
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 ()
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 (); :: 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 ; :: thesis: ( (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )
thus (a * b) * x = (a * b) \*\ c by ; :: thesis: a * (b * x) = a \*\ (b \*\ c)
b * x = b \*\ c by ;
hence a * (b * x) = a \*\ (b \*\ c) by Def6; :: thesis: verum