let x, y, z be Element of BOOLEAN * ; :: thesis: ( 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 ) ; :: thesis: (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 ; :: thesis: verum