let x, y be Element of BOOLEAN * ; :: thesis: ( x in rng Nat2BL & y in rng Nat2BL implies x + y = y + x )
assume AS: ( x in rng Nat2BL & y in rng Nat2BL ) ; :: thesis: x + y = y + x
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;
thus x + y = Nat2BL . (n + m) by A1, A2, LM100
.= y + x by A1, A2, LM100 ; :: thesis: verum