let N be non empty ConjNormAlgStr ; :: thesis: for a, b being Element of N st <%a,b%> is left_add-cancelable holds
( a is left_add-cancelable & b is left_add-cancelable )
let a, b be Element of N; :: thesis: ( <%a,b%> is left_add-cancelable implies ( a is left_add-cancelable & b is left_add-cancelable ) )
assume A1: <%a,b%> is left_add-cancelable ; :: thesis: ( a is left_add-cancelable & b is left_add-cancelable )
hereby :: according to ALGSTR_0:def 3 :: thesis: b is left_add-cancelable
let y, z be Element of N; :: thesis: ( a + y = a + z implies y = z )
assume A2: a + y = a + z ; :: thesis: y = z
<%a,b%> + <%y,(0. N)%> = <%(a + y),(b + (0. N))%> by Def9
.= <%a,b%> + <%z,(0. N)%> by A2, Def9 ;
then <%y,(0. N)%> = <%z,(0. N)%> by A1;
hence y = z by Th3; :: thesis: verum
end;
let y, z be Element of N; :: according to ALGSTR_0:def 3 :: thesis: ( not b + y = b + z or y = z )
assume A3: b + y = b + z ; :: thesis: y = z
<%a,b%> + <%(0. N),y%> = <%(a + (0. N)),(b + y)%> by Def9
.= <%a,b%> + <%(0. N),z%> by A3, Def9 ;
then <%(0. N),y%> = <%(0. N),z%> by A1;
hence y = z by Th3; :: thesis: verum