A1: now :: thesis: ( a = o & b = o & the multF of R . (x,x) <> x implies the multF of R . (x,x) is Element of carr (x,o) )

assume
( a = o & b = o & the multF of R . (x,x) <> x )
; :: thesis: the multF of R . (x,x) is Element of carr (x,o)

then not the multF of R . (x,x) in {x} by TARSKI:def 1;

then the multF of R . (x,x) in ([#] R) \ {x} by XBOOLE_0:def 5;

hence the multF of R . (x,x) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum

end;then not the multF of R . (x,x) in {x} by TARSKI:def 1;

then the multF of R . (x,x) in ([#] R) \ {x} by XBOOLE_0:def 5;

hence the multF of R . (x,x) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum

A2: now :: thesis: ( a <> o & b = o & the multF of R . (a,x) <> x implies the multF of R . (a,x) is Element of carr (x,o) )

assume A3:
( a <> o & b = o & the multF of R . (a,x) <> x )
; :: thesis: the multF of R . (a,x) is Element of carr (x,o)

then not a in {o} by TARSKI:def 1;

then a in ([#] R) \ {x} by XBOOLE_0:def 3;

then reconsider a1 = a as Element of [#] R ;

not the multF of R . (a,x) in {x} by A3, TARSKI:def 1;

then the multF of R . (a1,x) in ([#] R) \ {x} by XBOOLE_0:def 5;

hence the multF of R . (a,x) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum

end;then not a in {o} by TARSKI:def 1;

then a in ([#] R) \ {x} by XBOOLE_0:def 3;

then reconsider a1 = a as Element of [#] R ;

not the multF of R . (a,x) in {x} by A3, TARSKI:def 1;

then the multF of R . (a1,x) in ([#] R) \ {x} by XBOOLE_0:def 5;

hence the multF of R . (a,x) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum

A4: now :: thesis: ( a = o & b <> o & the multF of R . (x,b) <> x implies the multF of R . (x,b) is Element of carr (x,o) )

assume A5:
( a = o & b <> o & the multF of R . (x,b) <> x )
; :: thesis: the multF of R . (x,b) is Element of carr (x,o)

then not b in {o} by TARSKI:def 1;

then b in ([#] R) \ {x} by XBOOLE_0:def 3;

then reconsider b1 = b as Element of [#] R ;

not the multF of R . (x,b) in {x} by A5, TARSKI:def 1;

then the multF of R . (x,b1) in ([#] R) \ {x} by XBOOLE_0:def 5;

hence the multF of R . (x,b) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum

end;then not b in {o} by TARSKI:def 1;

then b in ([#] R) \ {x} by XBOOLE_0:def 3;

then reconsider b1 = b as Element of [#] R ;

not the multF of R . (x,b) in {x} by A5, TARSKI:def 1;

then the multF of R . (x,b1) in ([#] R) \ {x} by XBOOLE_0:def 5;

hence the multF of R . (x,b) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum

A6: now :: thesis: ( a <> o & b <> o & the multF of R . (a,b) <> x implies the multF of R . (a,b) is Element of carr (x,o) )

o in {o}
by TARSKI:def 1;assume A7:
( a <> o & b <> o & the multF of R . (a,b) <> x )
; :: thesis: the multF of R . (a,b) is Element of carr (x,o)

then not a in {o} by TARSKI:def 1;

then a in ([#] R) \ {x} by XBOOLE_0:def 3;

then reconsider a1 = a as Element of [#] R ;

not b in {o} by A7, TARSKI:def 1;

then b in ([#] R) \ {x} by XBOOLE_0:def 3;

then reconsider b1 = b as Element of [#] R ;

not the multF of R . (a,b) in {x} by A7, TARSKI:def 1;

then the multF of R . (a1,b1) in ([#] R) \ {x} by XBOOLE_0:def 5;

hence the multF of R . (a,b) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum

end;then not a in {o} by TARSKI:def 1;

then a in ([#] R) \ {x} by XBOOLE_0:def 3;

then reconsider a1 = a as Element of [#] R ;

not b in {o} by A7, TARSKI:def 1;

then b in ([#] R) \ {x} by XBOOLE_0:def 3;

then reconsider b1 = b as Element of [#] R ;

not the multF of R . (a,b) in {x} by A7, TARSKI:def 1;

then the multF of R . (a1,b1) in ([#] R) \ {x} by XBOOLE_0:def 5;

hence the multF of R . (a,b) is Element of carr (x,o) by XBOOLE_0:def 3; :: thesis: verum

hence ( ( a = o & b = o & the multF of R . (x,x) <> x implies the multF of R . (x,x) is Element of carr (x,o) ) & ( a <> o & b = o & the multF of R . (a,x) <> x implies the multF of R . (a,x) is Element of carr (x,o) ) & ( a = o & b <> o & the multF of R . (x,b) <> x implies the multF of R . (x,b) is Element of carr (x,o) ) & ( a <> o & b <> o & the multF of R . (a,b) <> x implies the multF of R . (a,b) is Element of carr (x,o) ) & ( ( not a = o or not b = o or not the multF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the multF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the multF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the multF of R . (a,b) <> x ) implies o is Element of carr (x,o) ) ) by A1, A2, A4, A6, XBOOLE_0:def 3; :: thesis: verum