:: ARYTM_0 semantic presentation

E1: {} in {{} }
by TARSKI:def 1;

E2: now
let c1 be set ;
assume E3: one = [0,c1] ;
{0} = 0 \/ {0}
.= succ 0 by ORDINAL1:def 1
.= {{0},{0,c1}} by E3, ORDINAL2:def 4, TARSKI:def 5 ;
then {0} in {0} by TARSKI:def 2;
hence not verum ;
end;

theorem E3: :: ARYTM_0:1
REAL+ c= REAL
proof
E4: REAL+ c= REAL+ \/ [:{{} },REAL+ :] by XBOOLE_1:7;
not [{} ,{} ] in REAL+ by ARYTM_2:3;
hence REAL+ c= REAL by E4, NUMBERS:def 1, ZFMISC_1:40;
end;

theorem E4: :: ARYTM_0:2
for b1 being Element of REAL+ holds
( b1 <> {} implies [{} ,b1] in REAL )
proof
let c1 be Element of REAL+ ;
assume E5: c1 <> {} ;
E6: now
assume [{} ,c1] in {[{} ,{} ]} ;
then [{} ,c1] = [{} ,{} ] by TARSKI:def 1;
hence not verum by E5, ZFMISC_1:33;
end;
{} in {{} } by TARSKI:def 1;
then [{} ,c1] in [:{{} },REAL+ :] by ZFMISC_1:106;
then [{} ,c1] in REAL+ \/ [:{{} },REAL+ :] by XBOOLE_0:def 2;
hence [{} ,c1] in REAL by E6, NUMBERS:def 1, XBOOLE_0:def 4;
end;

theorem E5: :: ARYTM_0:3
for b1 being set holds
not ( [{} ,b1] in REAL & not b1 <> {} )
proof
let c1 be set ;
assume that E6: [{} ,c1] in REAL
and E7: c1 = {} ;
[{} ,c1] in {[{} ,{} ]} by E7, TARSKI:def 1;
hence not verum by E6, NUMBERS:def 1, XBOOLE_0:def 4;
end;

theorem E6: :: ARYTM_0:4
for b1, b2 being Element of REAL+ holds b1 - b2 in REAL
proof
let c1, c2 be Element of REAL+ ;
per cases not ( not c2 <=' c1 & c2 <=' c1 ) ;
suppose c2 <=' c1 ;
then c1 - c2 = c1 -' c2 by ARYTM_1:def 2;
then c1 - c2 in REAL+ ;
hence c1 - c2 in REAL by E3;
end;
suppose E7: not c2 <=' c1 ;
then E8: c1 - c2 = [{} ,(c2 -' c1)] by ARYTM_1:def 2;
c2 -' c1 <> {} by E7, ARYTM_1:9;
hence c1 - c2 in REAL by E8, E4;
end;
end;
end;

theorem E7: :: ARYTM_0:5
REAL+ misses [:{{} },REAL+ :]
proof
assume REAL+ meets [:{{} },REAL+ :] ;
then consider c1 being set such that
E8: c1 in REAL+
and E9: c1 in [:{{} },REAL+ :] by XBOOLE_0:3;
consider c2, c3 being set such that
E10: c2 in {{} }
and E11: ( c3 in REAL+ & c1 = [c2,c3] ) by E9, ZFMISC_1:103;
c2 = {} by E10, TARSKI:def 1;
hence not verum by E8, E11, ARYTM_2:3;
end;

theorem E8: :: ARYTM_0:6
for b1, b2 being Element of REAL+ holds
( b1 - b2 = {} implies b1 = b2 )
proof
let c1, c2 be Element of REAL+ ;
E9: {} <> [{} ,(c2 -' c1)] ;
assume E10: c1 - c2 = {} ;
then E11: c2 <=' c1 by E9, ARYTM_1:def 2;
then c1 -' c2 = {} by E10, ARYTM_1:def 2;
hence c1 = c2 by E11, ARYTM_1:10;
end;

theorem E9: :: ARYTM_0:7
for b1, b2 being set holds
not one = [b1,b2]
proof
let c1, c2 be set ;
assume one = [c1,c2] ;
then E10: {{} } = {{c1,c2},{c1}} by ORDINAL3:18, TARSKI:def 5;
{c1} in {{c1,c2},{c1}} by TARSKI:def 2;
hence not verum by E10, TARSKI:def 1;
end;

theorem E10: :: ARYTM_0:8
for b1, b2, b3 being Element of REAL+ holds
( ( b1 *' b2 = b1 *' b3 ) implies ( not b1 <> {} or b2 = b3 ) )
proof
let c1, c2, c3 be Element of REAL+ ;
assume that E11: c1 <> {}
and E12: c1 *' c2 = c1 *' c3 ;
per cases ( c3 <=' c2 or c2 <=' c3 ) ;
suppose E13: c3 <=' c2 ;
then c1 *' (c2 -' c3) = (c1 *' c2) - (c1 *' c3) by ARYTM_1:26
.= {} by E12, ARYTM_1:18 ;
then {} = c2 -' c3 by E11, ARYTM_1:2
.= c2 - c3 by E13, ARYTM_1:def 2 ;
hence c2 = c3 by E8;
end;
suppose E13: c2 <=' c3 ;
then c1 *' (c3 -' c2) = (c1 *' c3) - (c1 *' c2) by ARYTM_1:26
.= {} by E12, ARYTM_1:18 ;
then {} = c3 -' c2 by E11, ARYTM_1:2
.= c3 - c2 by E13, ARYTM_1:def 2 ;
hence c2 = c3 by E8;
end;
end;
end;

definition
let c1, c2 be Element of REAL ;
canceled;
func + a1,a2 -> Element of REAL means :E11: :: ARYTM_0:def 2
ex b1, b2 being Element of REAL+ st
( a1 = b1 & a2 = b2 & a3 = b1 + b2 ) if ( a1 in REAL+ & a2 in REAL+ )
ex b1, b2 being Element of REAL+ st
( a1 = b1 & a2 = [0,b2] & a3 = b1 - b2 ) if ( a1 in REAL+ & a2 in [:{0},REAL+ :] )
ex b1, b2 being Element of REAL+ st
( a1 = [0,b1] & a2 = b2 & a3 = b2 - b1 ) if ( a2 in REAL+ & a1 in [:{0},REAL+ :] )
otherwise ex b1, b2 being Element of REAL+ st
( a1 = [0,b1] & a2 = [0,b2] & a3 = [0,(b1 + b2)] );
existence
( not ( c1 in REAL+ & c2 in REAL+ & for b1 being Element of REAL
for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = b3 & b1 = b2 + b3 ) ) & not ( c1 in REAL+ & c2 in [:{0},REAL+ :] & for b1 being Element of REAL
for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = [0,b3] & b1 = b2 - b3 ) ) & not ( c2 in REAL+ & c1 in [:{0},REAL+ :] & for b1 being Element of REAL
for b2, b3 being Element of REAL+ holds
not ( c1 = [0,b2] & c2 = b3 & b1 = b3 - b2 ) ) & not ( not ( c1 in REAL+ & c2 in REAL+ ) & not ( c1 in REAL+ & c2 in [:{0},REAL+ :] ) & not ( c2 in REAL+ & c1 in [:{0},REAL+ :] ) & for b1 being Element of REAL
for b2, b3 being Element of REAL+ holds
not ( c1 = [0,b2] & c2 = [0,b3] & b1 = [0,(b2 + b3)] ) ) )
proof
hereby
assume ( c1 in REAL+ & c2 in REAL+ ) ;
then reconsider c3 = c1, c4 = c2 as Element of REAL+ ;
c3 + c4 in REAL+ ;
then reconsider c5 = c3 + c4 as Element of REAL by E3;
take c6 = c5;
take c7 = c3;
take c8 = c4;
thus ( c1 = c7 & c2 = c8 & c6 = c7 + c8 ) ;
end;
hereby
assume c1 in REAL+ ;
then reconsider c3 = c1 as Element of REAL+ ;
assume c2 in [:{0},REAL+ :] ;
then consider c4, c5 being set such that
E11: c4 in {0}
and E12: c5 in REAL+
and E13: c2 = [c4,c5] by ZFMISC_1:103;
reconsider c6 = c5 as Element of REAL+ by E12;
reconsider c7 = c3 - c6 as Element of REAL by E6;
take c8 = c7;
take c9 = c3;
take c10 = c6;
thus ( c1 = c9 & c2 = [0,c10] & c8 = c9 - c10 ) by E11, E13, TARSKI:def 1;
end;
hereby
assume c2 in REAL+ ;
then reconsider c3 = c2 as Element of REAL+ ;
assume c1 in [:{0},REAL+ :] ;
then consider c4, c5 being set such that
E11: c4 in {0}
and E12: c5 in REAL+
and E13: c1 = [c4,c5] by ZFMISC_1:103;
reconsider c6 = c5 as Element of REAL+ by E12;
reconsider c7 = c3 - c6 as Element of REAL by E6;
take c8 = c7;
take c9 = c6;
take c10 = c3;
thus ( c1 = [0,c9] & c2 = c10 & c8 = c10 - c9 ) by E11, E13, TARSKI:def 1;
end; ( c1 in REAL+ \/ [:{0},REAL+ :] & c2 in REAL+ \/ [:{0},REAL+ :] ) by NUMBERS:def 1, XBOOLE_0:def 4;
then E11: ( ( c1 in REAL+ or c1 in [:{0},REAL+ :] ) & ( c2 in REAL+ or c2 in [:{0},REAL+ :] ) ) by XBOOLE_0:def 2;
assume E12: ( not ( c1 in REAL+ & c2 in REAL+ ) & not ( c1 in REAL+ & c2 in [:{0},REAL+ :] ) & not ( c2 in REAL+ & c1 in [:{0},REAL+ :] ) ) ;
then consider c3, c4 being set such that
E13: c3 in {0}
and E14: c4 in REAL+
and E15: c1 = [c3,c4] by E11, ZFMISC_1:103;
reconsider c5 = c4 as Element of REAL+ by E14;
consider c6, c7 being set such that
E16: c6 in {0}
and E17: c7 in REAL+
and E18: c2 = [c6,c7] by E11, E12, ZFMISC_1:103;
reconsider c8 = c7 as Element of REAL+ by E17;
c1 = [0,c5] by E13, E15, TARSKI:def 1;
then c5 <> 0 by E5;
then c5 + c8 <> 0 by ARYTM_2:6;
then reconsider c9 = [0,(c8 + c5)] as Element of REAL by E4;
take c9 ;
take c5 ;
take c8 ;
thus ( c1 = [0,c5] & c2 = [0,c8] & c9 = [0,(c5 + c8)] ) by E13, E15, E16, E18, TARSKI:def 1;
end;
uniqueness
for b1, b2 being Element of REAL holds
( ( ( c1 in REAL+ & c2 in REAL+ ) implies ( for b3, b4 being Element of REAL+ holds
not ( c1 = b3 & c2 = b4 & b1 = b3 + b4 ) or for b3, b4 being Element of REAL+ holds
not ( c1 = b3 & c2 = b4 & b2 = b3 + b4 ) or b1 = b2 ) ) & ( ( c1 in REAL+ & c2 in [:{0},REAL+ :] ) implies ( for b3, b4 being Element of REAL+ holds
not ( c1 = b3 & c2 = [0,b4] & b1 = b3 - b4 ) or for b3, b4 being Element of REAL+ holds
not ( c1 = b3 & c2 = [0,b4] & b2 = b3 - b4 ) or b1 = b2 ) ) & ( ( c2 in REAL+ & c1 in [:{0},REAL+ :] ) implies ( for b3, b4 being Element of REAL+ holds
not ( c1 = [0,b3] & c2 = b4 & b1 = b4 - b3 ) or for b3, b4 being Element of REAL+ holds
not ( c1 = [0,b3] & c2 = b4 & b2 = b4 - b3 ) or b1 = b2 ) ) & ( ( ) implies ( ( c1 in REAL+ & c2 in REAL+ ) or ( c1 in REAL+ & c2 in [:{0},REAL+ :] ) or ( c2 in REAL+ & c1 in [:{0},REAL+ :] ) or for b3, b4 being Element of REAL+ holds
not ( c1 = [0,b3] & c2 = [0,b4] & b1 = [0,(b3 + b4)] ) or for b3, b4 being Element of REAL+ holds
not ( c1 = [0,b3] & c2 = [0,b4] & b2 = [0,(b3 + b4)] ) or b1 = b2 ) ) )
proof
let c3, c4 be Element of REAL ;
thus ( ( c1 in REAL+ & c2 in REAL+ ) implies ( for b1, b2 being Element of REAL+ holds
not ( c1 = b1 & c2 = b2 & c3 = b1 + b2 ) or for b1, b2 being Element of REAL+ holds
not ( c1 = b1 & c2 = b2 & c4 = b1 + b2 ) or c3 = c4 ) ) ;
thus ( ( c1 in REAL+ & c2 in [:{0},REAL+ :] ) implies ( for b1, b2 being Element of REAL+ holds
not ( c1 = b1 & c2 = [0,b2] & c3 = b1 - b2 ) or for b1, b2 being Element of REAL+ holds
not ( c1 = b1 & c2 = [0,b2] & c4 = b1 - b2 ) or c3 = c4 ) ) by ZFMISC_1:33;
thus ( ( c2 in REAL+ & c1 in [:{0},REAL+ :] ) implies ( for b1, b2 being Element of REAL+ holds
not ( c1 = [0,b1] & c2 = b2 & c3 = b2 - b1 ) or for b1, b2 being Element of REAL+ holds
not ( c1 = [0,b1] & c2 = b2 & c4 = b2 - b1 ) or c3 = c4 ) ) by ZFMISC_1:33;
assume ( not ( c1 in REAL+ & c2 in REAL+ ) & not ( c1 in REAL+ & c2 in [:{0},REAL+ :] ) & not ( c2 in REAL+ & c1 in [:{0},REAL+ :] ) ) ;
given c5, c6 being Element of REAL+ such that E11: ( c1 = [0,c5] & c2 = [0,c6] )
and E12: c3 = [0,(c5 + c6)] ;
given c7, c8 being Element of REAL+ such that E13: ( c1 = [0,c7] & c2 = [0,c8] )
and E14: c4 = [0,(c7 + c8)] ;
( c5 = c7 & c6 = c8 ) by E11, E13, ZFMISC_1:33;
hence c3 = c4 by E12, E14;
end;
consistency
for b1 being Element of REAL holds
( ( ( c1 in REAL+ & c2 in REAL+ & c1 in REAL+ & c2 in [:{0},REAL+ :] ) implies ( ( not ( ex b2, b3 being Element of REAL+ st
( c1 = b2 & c2 = b3 & b1 = b2 + b3 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = [0,b3] & b1 = b2 - b3 ) ) & not ( ex b2, b3 being Element of REAL+ st
( c1 = b2 & c2 = [0,b3] & b1 = b2 - b3 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = b3 & b1 = b2 + b3 ) ) ) ) ) & ( ( c1 in REAL+ & c2 in REAL+ & c2 in REAL+ & c1 in [:{0},REAL+ :] ) implies ( ( not ( ex b2, b3 being Element of REAL+ st
( c1 = b2 & c2 = b3 & b1 = b2 + b3 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = [0,b2] & c2 = b3 & b1 = b3 - b2 ) ) & not ( ex b2, b3 being Element of REAL+ st
( c1 = [0,b2] & c2 = b3 & b1 = b3 - b2 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = b3 & b1 = b2 + b3 ) ) ) ) ) & ( ( c1 in REAL+ & c2 in [:{0},REAL+ :] & c2 in REAL+ & c1 in [:{0},REAL+ :] ) implies ( ( not ( ex b2, b3 being Element of REAL+ st
( c1 = b2 & c2 = [0,b3] & b1 = b2 - b3 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = [0,b2] & c2 = b3 & b1 = b3 - b2 ) ) & not ( ex b2, b3 being Element of REAL+ st
( c1 = [0,b2] & c2 = b3 & b1 = b3 - b2 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = [0,b3] & b1 = b2 - b3 ) ) ) ) ) ) by E7, XBOOLE_0:3;
commutativity
for b1, b2, b3 being Element of REAL holds
( ( ) implies ( ( b2 in REAL+ & b3 in REAL+ & for b4, b5 being Element of REAL+ holds
not ( b2 = b4 & b3 = b5 & b1 = b4 + b5 ) ) or ( b2 in REAL+ & b3 in [:{0},REAL+ :] & for b4, b5 being Element of REAL+ holds
not ( b2 = b4 & b3 = [0,b5] & b1 = b4 - b5 ) ) or ( b3 in REAL+ & b2 in [:{0},REAL+ :] & for b4, b5 being Element of REAL+ holds
not ( b2 = [0,b4] & b3 = b5 & b1 = b5 - b4 ) ) or ( not ( b2 in REAL+ & b3 in REAL+ ) & not ( b2 in REAL+ & b3 in [:{0},REAL+ :] ) & not ( b3 in REAL+ & b2 in [:{0},REAL+ :] ) & for b4, b5 being Element of REAL+ holds
not ( b2 = [0,b4] & b3 = [0,b5] & b1 = [0,(b4 + b5)] ) ) or ( not ( b3 in REAL+ & b2 in REAL+ & for b4, b5 being Element of REAL+ holds
not ( b3 = b4 & b2 = b5 & b1 = b4 + b5 ) ) & not ( b3 in REAL+ & b2 in [:{0},REAL+ :] & for b4, b5 being Element of REAL+ holds
not ( b3 = b4 & b2 = [0,b5] & b1 = b4 - b5 ) ) & not ( b2 in REAL+ & b3 in [:{0},REAL+ :] & for b4, b5 being Element of REAL+ holds
not ( b3 = [0,b4] & b2 = b5 & b1 = b5 - b4 ) ) & not ( not ( b3 in REAL+ & b2 in REAL+ ) & not ( b3 in REAL+ & b2 in [:{0},REAL+ :] ) & not ( b2 in REAL+ & b3 in [:{0},REAL+ :] ) & for b4, b5 being Element of REAL+ holds
not ( b3 = [0,b4] & b2 = [0,b5] & b1 = [0,(b4 + b5)] ) ) ) ) ) ;
func * a1,a2 -> Element of REAL means :E12: :: ARYTM_0:def 3
ex b1, b2 being Element of REAL+ st
( a1 = b1 & a2 = b2 & a3 = b1 *' b2 ) if ( a1 in REAL+ & a2 in REAL+ )
ex b1, b2 being Element of REAL+ st
( a1 = b1 & a2 = [0,b2] & a3 = [0,(b1 *' b2)] ) if ( a1 in REAL+ & a2 in [:{0},REAL+ :] & a1 <> 0 )
ex b1, b2 being Element of REAL+ st
( a1 = [0,b1] & a2 = b2 & a3 = [0,(b2 *' b1)] ) if ( a2 in REAL+ & a1 in [:{0},REAL+ :] & a2 <> 0 )
ex b1, b2 being Element of REAL+ st
( a1 = [0,b1] & a2 = [0,b2] & a3 = b2 *' b1 ) if ( a1 in [:{0},REAL+ :] & a2 in [:{0},REAL+ :] )
otherwise a3 = 0;
existence
( not ( c1 in REAL+ & c2 in REAL+ & for b1 being Element of REAL
for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = b3 & b1 = b2 *' b3 ) ) & not ( c1 in REAL+ & c2 in [:{0},REAL+ :] & c1 <> 0 & for b1 being Element of REAL
for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = [0,b3] & b1 = [0,(b2 *' b3)] ) ) & not ( c2 in REAL+ & c1 in [:{0},REAL+ :] & c2 <> 0 & for b1 being Element of REAL
for b2, b3 being Element of REAL+ holds
not ( c1 = [0,b2] & c2 = b3 & b1 = [0,(b3 *' b2)] ) ) & not ( c1 in [:{0},REAL+ :] & c2 in [:{0},REAL+ :] & for b1 being Element of REAL
for b2, b3 being Element of REAL+ holds
not ( c1 = [0,b2] & c2 = [0,b3] & b1 = b3 *' b2 ) ) & not ( not ( c1 in REAL+ & c2 in REAL+ ) & not ( c1 in REAL+ & c2 in [:{0},REAL+ :] & c1 <> 0 ) & not ( c2 in REAL+ & c1 in [:{0},REAL+ :] & c2 <> 0 ) & not ( c1 in [:{0},REAL+ :] & c2 in [:{0},REAL+ :] ) & for b1 being Element of REAL holds
not b1 = 0 ) )
proof
hereby
assume ( c1 in REAL+ & c2 in REAL+ ) ;
then reconsider c3 = c1, c4 = c2 as Element of REAL+ ;
c3 *' c4 in REAL+ ;
then reconsider c5 = c3 *' c4 as Element of REAL by E3;
take c6 = c5;
take c7 = c3;
take c8 = c4;
thus ( c1 = c7 & c2 = c8 & c6 = c7 *' c8 ) ;
end;
hereby
assume c1 in REAL+ ;
then reconsider c3 = c1 as Element of REAL+ ;
assume c2 in [:{0},REAL+ :] ;
then consider c4, c5 being set such that
E11: c4 in {0}
and E12: c5 in REAL+
and E13: c2 = [c4,c5] by ZFMISC_1:103;
reconsider c6 = c5 as Element of REAL+ by E12;
assume E14: c1 <> 0 ;
c2 = [0,c6] by E11, E13, TARSKI:def 1;
then c6 <> 0 by E5;
then c3 *' c6 <> 0 by E14, ARYTM_1:2;
then reconsider c7 = [0,(c3 *' c6)] as Element of REAL by E4;
take c8 = c7;
take c9 = c3;
take c10 = c6;
thus ( c1 = c9 & c2 = [0,c10] & c8 = [0,(c9 *' c10)] ) by E11, E13, TARSKI:def 1;
end;
hereby
assume c2 in REAL+ ;
then reconsider c3 = c2 as Element of REAL+ ;
assume c1 in [:{0},REAL+ :] ;
then consider c4, c5 being set such that
E11: c4 in {0}
and E12: c5 in REAL+
and E13: c1 = [c4,c5] by ZFMISC_1:103;
reconsider c6 = c5 as Element of REAL+ by E12;
assume E14: c2 <> 0 ;
c1 = [0,c6] by E11, E13, TARSKI:def 1;
then c6 <> 0 by E5;
then c6 *' c3 <> 0 by E14, ARYTM_1:2;
then reconsider c7 = [0,(c3 *' c6)] as Element of REAL by E4;
take c8 = c7;
take c9 = c6;
take c10 = c3;
thus ( c1 = [0,c9] & c2 = c10 & c8 = [0,(c10 *' c9)] ) by E11, E13, TARSKI:def 1;
end;
hereby
assume c1 in [:{0},REAL+ :] ;
then consider c3, c4 being set such that
E11: c3 in {0}
and E12: c4 in REAL+
and E13: c1 = [c3,c4] by ZFMISC_1:103;
reconsider c5 = c4 as Element of REAL+ by E12;
assume c2 in [:{0},REAL+ :] ;
then consider c6, c7 being set such that
E14: c6 in {0}
and E15: c7 in REAL+
and E16: c2 = [c6,c7] by ZFMISC_1:103;
reconsider c8 = c7 as Element of REAL+ by E15;
c5 *' c8 in REAL+ ;
then reconsider c9 = c8 *' c5 as Element of REAL by E3;
take c10 = c9;
take c11 = c5;
take c12 = c8;
thus ( c1 = [0,c11] & c2 = [0,c12] & c10 = c12 *' c11 ) by E11, E13, E14, E16, TARSKI:def 1;
end; thus not ( not ( c1 in REAL+ & c2 in REAL+ ) & not ( c1 in REAL+ & c2 in [:{0},REAL+ :] & c1 <> 0 ) & not ( c2 in REAL+ & c1 in [:{0},REAL+ :] & c2 <> 0 ) & not ( c1 in [:{0},REAL+ :] & c2 in [:{0},REAL+ :] ) & for b1 being Element of REAL holds
not b1 = 0 ) by E3, ARYTM_2:21;
end;
uniqueness
for b1, b2 being Element of REAL holds
( ( ( c1 in REAL+ & c2 in REAL+ ) implies ( for b3, b4 being Element of REAL+ holds
not ( c1 = b3 & c2 = b4 & b1 = b3 *' b4 ) or for b3, b4 being Element of REAL+ holds
not ( c1 = b3 & c2 = b4 & b2 = b3 *' b4 ) or b1 = b2 ) ) & ( ( c1 in REAL+ & c2 in [:{0},REAL+ :] ) implies ( not c1 <> 0 or for b3, b4 being Element of REAL+ holds
not ( c1 = b3 & c2 = [0,b4] & b1 = [0,(b3 *' b4)] ) or for b3, b4 being Element of REAL+ holds
not ( c1 = b3 & c2 = [0,b4] & b2 = [0,(b3 *' b4)] ) or b1 = b2 ) ) & ( ( c2 in REAL+ & c1 in [:{0},REAL+ :] ) implies ( not c2 <> 0 or for b3, b4 being Element of REAL+ holds
not ( c1 = [0,b3] & c2 = b4 & b1 = [0,(b4 *' b3)] ) or for b3, b4 being Element of REAL+ holds
not ( c1 = [0,b3] & c2 = b4 & b2 = [0,(b4 *' b3)] ) or b1 = b2 ) ) & ( ( c1 in [:{0},REAL+ :] & c2 in [:{0},REAL+ :] ) implies ( for b3, b4 being Element of REAL+ holds
not ( c1 = [0,b3] & c2 = [0,b4] & b1 = b4 *' b3 ) or for b3, b4 being Element of REAL+ holds
not ( c1 = [0,b3] & c2 = [0,b4] & b2 = b4 *' b3 ) or b1 = b2 ) ) & ( ( b1 = 0 & b2 = 0 ) implies ( ( c1 in REAL+ & c2 in REAL+ ) or ( c1 in REAL+ & c2 in [:{0},REAL+ :] & c1 <> 0 ) or ( c2 in REAL+ & c1 in [:{0},REAL+ :] & c2 <> 0 ) or ( c1 in [:{0},REAL+ :] & c2 in [:{0},REAL+ :] ) or b1 = b2 ) ) )
proof
let c3, c4 be Element of REAL ;
thus ( ( c1 in REAL+ & c2 in REAL+ ) implies ( for b1, b2 being Element of REAL+ holds
not ( c1 = b1 & c2 = b2 & c3 = b1 *' b2 ) or for b1, b2 being Element of REAL+ holds
not ( c1 = b1 & c2 = b2 & c4 = b1 *' b2 ) or c3 = c4 ) ) ;
thus ( ( c1 in REAL+ & c2 in [:{0},REAL+ :] ) implies ( not c1 <> 0 or for b1, b2 being Element of REAL+ holds
not ( c1 = b1 & c2 = [0,b2] & c3 = [0,(b1 *' b2)] ) or for b1, b2 being Element of REAL+ holds
not ( c1 = b1 & c2 = [0,b2] & c4 = [0,(b1 *' b2)] ) or c3 = c4 ) ) by ZFMISC_1:33;
thus ( ( c2 in REAL+ & c1 in [:{0},REAL+ :] ) implies ( not c2 <> 0 or for b1, b2 being Element of REAL+ holds
not ( c1 = [0,b1] & c2 = b2 & c3 = [0,(b2 *' b1)] ) or for b1, b2 being Element of REAL+ holds
not ( c1 = [0,b1] & c2 = b2 & c4 = [0,(b2 *' b1)] ) or c3 = c4 ) ) by ZFMISC_1:33;
hereby
assume ( c1 in [:{0},REAL+ :] & c2 in [:{0},REAL+ :] ) ;
given c5, c6 being Element of REAL+ such that E11: ( c1 = [0,c5] & c2 = [0,c6] )
and E12: c3 = c6 *' c5 ;
given c7, c8 being Element of REAL+ such that E13: ( c1 = [0,c7] & c2 = [0,c8] )
and E14: c4 = c8 *' c7 ;
( c5 = c7 & c6 = c8 ) by E11, E13, ZFMISC_1:33;
hence c3 = c4 by E12, E14;
end; thus ( ( c3 = 0 & c4 = 0 ) implies ( ( c1 in REAL+ & c2 in REAL+ ) or ( c1 in REAL+ & c2 in [:{0},REAL+ :] & c1 <> 0 ) or ( c2 in REAL+ & c1 in [:{0},REAL+ :] & c2 <> 0 ) or ( c1 in [:{0},REAL+ :] & c2 in [:{0},REAL+ :] ) or c3 = c4 ) ) ;
end;
consistency
for b1 being Element of REAL holds
( ( ( c1 in REAL+ & c2 in REAL+ & c1 in REAL+ & c2 in [:{0},REAL+ :] ) implies ( not c1 <> 0 or ( not ( ex b2, b3 being Element of REAL+ st
( c1 = b2 & c2 = b3 & b1 = b2 *' b3 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = [0,b3] & b1 = [0,(b2 *' b3)] ) ) & not ( ex b2, b3 being Element of REAL+ st
( c1 = b2 & c2 = [0,b3] & b1 = [0,(b2 *' b3)] ) & for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = b3 & b1 = b2 *' b3 ) ) ) ) ) & ( ( c1 in REAL+ & c2 in REAL+ & c2 in REAL+ & c1 in [:{0},REAL+ :] ) implies ( not c2 <> 0 or ( not ( ex b2, b3 being Element of REAL+ st
( c1 = b2 & c2 = b3 & b1 = b2 *' b3 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = [0,b2] & c2 = b3 & b1 = [0,(b3 *' b2)] ) ) & not ( ex b2, b3 being Element of REAL+ st
( c1 = [0,b2] & c2 = b3 & b1 = [0,(b3 *' b2)] ) & for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = b3 & b1 = b2 *' b3 ) ) ) ) ) & ( ( c1 in REAL+ & c2 in REAL+ & c1 in [:{0},REAL+ :] & c2 in [:{0},REAL+ :] ) implies ( ( not ( ex b2, b3 being Element of REAL+ st
( c1 = b2 & c2 = b3 & b1 = b2 *' b3 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = [0,b2] & c2 = [0,b3] & b1 = b3 *' b2 ) ) & not ( ex b2, b3 being Element of REAL+ st
( c1 = [0,b2] & c2 = [0,b3] & b1 = b3 *' b2 ) & for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 = b3 & b1 = b2 *' b3 ) ) ) ) ) & ( ( c1 in REAL+ & c2 in [:{0},REAL+ :] & c2 in REAL+ & c1 in [:{0},REAL+ :] ) implies ( not c1 <> 0 or not c2 <> 0 or ( not ( ex b2, b3 being Element of REAL+ st
( c1 = b2 & c2 = [0,b3] & b1 = [0,(b2 *' b3)] ) & for b2, b3 being Element of REAL+ holds
not ( c1 = [0,b2] & c2 = b3 & b1 = [0,(b3 *' b2)] ) ) & not ( ex b2, b3 being Element of REAL+ st
( c1 = [0,b2] & c2 = b3 & b1 = [0,(b3 *' b2)] ) & for b2, b3 being Element of REAL+ holds
not ( c1 = b2 & c2 =