:: ARYTM_0 semantic presentation

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

Lemma2: 1 = succ 0
;

theorem Th1: :: 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 Th2: :: 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 Th3: :: 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 Th4: :: 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 Th1;
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, Th2;
end;
end;
end;

theorem Th5: :: 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 Th6: :: 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 Th7: :: ARYTM_0:7
for b1, b2 being set holds
not 1 = [b1,b2]
proof
let c1, c2 be set ;
assume 1 = [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 Th8: :: ARYTM_0:8
for b1, b2, b3 being Element of REAL+ holds
( b1 <> {} & b1 *' b2 = b1 *' b3 implies 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 Th6;
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 Th6;
end;
end;
end;

definition
let c1, c2 be Element of REAL ;
canceled;
func + c1,c2 -> Element of REAL means :Def2: :: 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 Th1;
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 Th4;
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 Th4;
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 Th3;
then c5 + c8 <> 0 by ARYTM_2:6;
then reconsider c9 = [0,(c8 + c5)] as Element of REAL by Th2;
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+ & ex b3, b4 being Element of REAL+ st
( c1 = b3 & c2 = b4 & b1 = b3 + b4 ) & ex b3, b4 being Element of REAL+ st
( c1 = b3 & c2 = b4 & b2 = b3 + b4 ) implies b1 = b2 ) & ( c1 in REAL+ & c2 in [:{0},REAL+ :] & ex b3, b4 being Element of REAL+ st
( c1 = b3 & c2 = [0,b4] & b1 = b3 - b4 ) & ex b3, b4 being Element of REAL+ st
( c1 = b3 & c2 = [0,b4] & b2 = b3 - b4 ) implies b1 = b2 ) & ( c2 in REAL+ & c1 in [:{0},REAL+ :] & ex b3, b4 being Element of REAL+ st
( c1 = [0,b3] & c2 = b4 & b1 = b4 - b3 ) & ex b3, b4 being Element of REAL+ st
( c1 = [0,b3] & c2 = b4 & b2 = b4 - b3 ) implies b1 = b2 ) & ( not ( c1 in REAL+ & c2 in REAL+ ) & not ( c1 in REAL+ & c2 in [:{0},REAL+ :] ) & not ( c2 in REAL+ & c1 in [:{0},REAL+ :] ) & ex b3, b4 being Element of REAL+ st
( c1 = [0,b3] & c2 = [0,b4] & b1 = [0,(b3 + b4)] ) & ex b3, b4 being Element of REAL+ st
( c1 = [0,b3] & c2 = [0,b4] & b2 = [0,(b3 + b4)] ) implies b1 = b2 ) )
proof
let c3, c4 be Element of REAL ;
thus ( c1 in REAL+ & c2 in REAL+ & ex b1, b2 being Element of REAL+ st
( c1 = b1 & c2 = b2 & c3 = b1 + b2 ) & ex b1, b2 being Element of REAL+ st
( c1 = b1 & c2 = b2 & c4 = b1 + b2 ) implies c3 = c4 ) ;
thus ( c1 in REAL+ & c2 in [:{0},REAL+ :] & ex b1, b2 being Element of REAL+ st
( c1 = b1 & c2 = [0,b2] & c3 = b1 - b2 ) & ex b1, b2 being Element of REAL+ st
( c1 = b1 & c2 = [0,b2] & c4 = b1 - b2 ) implies c3 = c4 ) by ZFMISC_1:33;
thus ( c2 in REAL+ & c1 in [:{0},REAL+ :] & ex b1, b2 being Element of REAL+ st
( c1 = [0,b1] & c2 = b2 & c3 = b2 - b1 ) & ex b1, b2 being Element of REAL+ st
( c1 = [0,b1] & c2 = b2 & c4 = b2 - b1 ) implies 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 Th5, XBOOLE_0:3;
commutativity
for b1, b2, b3 being Element of REAL holds
( not ( b2 in REAL+ & b3 in REAL+ & ( for b4, b5 being Element of REAL+ holds
not ( b2 = b4 & b3 = b5 & b1 = b4 + b5 ) ) ) & not ( b2 in REAL+ & b3 in [:{0},REAL+ :] & ( for b4, b5 being Element of REAL+ holds
not ( b2 = b4 & b3 = [0,b5] & b1 = b4 - b5 ) ) ) & not ( b3 in REAL+ & b2 in [:{0},REAL+ :] & ( for b4, b5 being Element of REAL+ holds
not ( b2 = [0,b4] & b3 = b5 & b1 = b5 - b4 ) ) ) & not ( 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)] ) ) ) implies ( 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 * c1,c2 -> Element of REAL means :Def3: :: 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 Th1;
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 Th3;
then c3 *' c6 <> 0 by E14, ARYTM_1:2;
then reconsider c7 = [0,(c3 *' c6)] as Element of REAL by Th2;
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 Th3;
then c6 *' c3 <> 0 by E14, ARYTM_1:2;
then reconsider c7 = [0,(c3 *' c6)] as Element of REAL by Th2;
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 Th1;
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 Th1, ARYTM_2:21;
end;
uniqueness
for b1, b2 being Element of REAL holds
( ( c1 in REAL+ & c2 in REAL+ & ex b3, b4 being Element of REAL+ st
( c1 = b3 & c2 = b4 & b1 = b3 *' b4 ) & ex b3, b4 being Element of REAL+ st
( c1 = b3 & c2 = b4 & b2 = b3 *' b4 ) implies b1 = b2 ) & ( c1 in REAL+ & c2 in [:{0},REAL+ :] & c1 <> 0 & ex b3, b4 being Element of REAL+ st
( c1 = b3 & c2 = [0,b4] & b1 = [0,(b3 *' b4)] ) & ex b3, b4 being Element of REAL+ st
( c1 = b3 & c2 = [0,b4] & b2 = [0,(b3 *' b4)] ) implies b1 = b2 ) & ( c2 in REAL+ & c1 in [:{0},REAL+ :] & c2 <> 0 & ex b3, b4 being Element of REAL+ st
( c1 = [0,b3] & c2 = b4 & b1 = [0,(b4 *' b3)] ) & ex b3, b4 being Element of REAL+ st
( c1 = [0,b3] & c2 = b4 & b2 = [0,(b4 *' b3)] ) implies b1 = b2 ) & ( c1 in [:{0},REAL+ :] & c2 in [:{0},REAL+ :] & ex b3, b4 being Element of REAL+ st
( c1 = [0,b3] & c2 = [0,b4] & b1 = b4 *' b3 ) & ex b3, b4 being Element of REAL+ st
( c1 = [0,b3] & c2 = [0,b4] & b2 = b4 *' b3 ) implies b1 = b2 ) & ( 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+ :] ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
let c3, c4 be Element of REAL ;
thus ( c1 in REAL+ & c2 in REAL+ & ex b1, b2 being Element of REAL+ st
( c1 = b1 & c2 = b2 & c3 = b1 *' b2 ) & ex b1, b2 being Element of REAL+ st
( c1 = b1 & c2 = b2 & c4 = b1 *' b2 ) implies c3 = c4 ) ;
thus ( c1 in REAL+ & c2 in [:{0},REAL+ :] & c1 <> 0 & ex b1, b2 being Element of REAL+ st
( c1 = b1 & c2 = [0,b2] & c3 = [0,(b1 *' b2)] ) & ex b1, b2 being Element of REAL+ st
( c1 = b1 & c2 = [0,b2] & c4 = [0,(b1 *' b2)] ) implies c3 = c4 ) by ZFMISC_1:33;
thus ( c2 in REAL+ & c1 in [:{0},REAL+ :] & c2 <> 0 & ex b1, b2 being Element of REAL+ st
( c1 = [0,b1] & c2 = b2 & c3 = [0,(b2 *' b1)] ) & ex b1, b2 being Element of REAL+ st
( c1 = [0,b1] & c2 = b2 & c4 = [0,(b2 *' b1)] ) implies 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 ( 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+ :] ) & c3 = 0 & c4 = 0 implies c3 = c4 ) ;
end;
consistency
for b1 being Element of REAL holds
( ( c1 in REAL+ & c2 in REAL+ & c1 in REAL+ & c2 in [:{0},REAL+ :] & c1 <> 0 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 = [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 [: