let x, y, z be Element of BOOLEAN * ; ( x in rng Nat2BL & y in rng Nat2BL & z in rng Nat2BL implies (x + y) + z = x + (y + z) )
assume AS:
( x in rng Nat2BL & y in rng Nat2BL & z in rng Nat2BL )
; (x + y) + z = x + (y + z)
then consider n being Element of NAT such that
A1:
x = Nat2BL . n
by FUNCT_2:113;
consider m being Element of NAT such that
A2:
y = Nat2BL . m
by AS, FUNCT_2:113;
consider k being Element of NAT such that
A3:
z = Nat2BL . k
by AS, FUNCT_2:113;
reconsider nm = n + m as Element of NAT by ORDINAL1:def 12;
reconsider mk = m + k as Element of NAT by ORDINAL1:def 12;
thus (x + y) + z =
(Nat2BL . nm) + (Nat2BL . k)
by LM100, A1, A2, A3
.=
Nat2BL . ((n + m) + k)
by LM100
.=
Nat2BL . (n + mk)
.=
(Nat2BL . n) + (Nat2BL . mk)
by LM100
.=
x + (y + z)
by A1, A2, A3, LM100
; verum