:: ARYTM_0 semantic presentation

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

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

theorem E3: :: ARYTM_0:2
for b1 being Element of REAL+ holds
( b1 <> {} implies [{} ,b1] in REAL )
proof
let c1 be Element of REAL+ ;
assume E4: c1 <> {} ;
E5: now
assume [{} ,c1] in {[{} ,{} ]} ;
then [{} ,c1] = [{} ,{} ] by TARSKI:def 1;
hence not verum by E4, 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 E5, NUMBERS:def 1, XBOOLE_0:def 4;
end;

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

theorem E5: :: 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 E2;
end;
suppose E6: not c2 <=' c1 ;
then E7: c1 - c2 = [{} ,(c2 -' c1)] by ARYTM_1:def 2;
c2 -' c1 <> {} by E6, ARYTM_1:9;
hence c1 - c2 in REAL by E7, E3;
end;
end;
end;

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

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

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

theorem E9: :: 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
E10: c1 <> {} and
E11: c1 *' c2 = c1 *' c3 ;
per cases ( c3 <=' c2 or c2 <=' c3 ) ;
suppose E12: c3 <=' c2 ;
then c1 *' (c2 -' c3) = (c1 *' c2) - (c1 *' c3) by ARYTM_1:26
.= {} by E11, ARYTM_1:18 ;
then {} = c2 -' c3 by E10, ARYTM_1:2
.= c2 - c3 by E12, ARYTM_1:def 2 ;
hence c2 = c3 by E7;
end;
suppose E12: c2 <=' c3 ;
then c1 *' (c3 -' c2) = (c1 *' c3) - (c1 *' c2) by ARYTM_1:26
.= {} by E11, ARYTM_1:18 ;
then {} = c3 -' c2 by E10, ARYTM_1:2
.= c3 - c2 by E12, ARYTM_1:def 2 ;
hence c2 = c3 by E7;
end;
end;
end;

definition
let c1, c2 be Element of REAL ;
canceled;
func + c1,c2 -> Element of REAL means :E10: :: 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 E2;
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
E10: c4 in {0} and
E11: c5 in REAL+ and
E12: c2 = [c4,c5] by ZFMISC_1:103;
reconsider c6 = c5 as Element of REAL+ by E11;
reconsider c7 = c3 - c6 as Element of REAL by E5;
take c8 = c7;
take c9 = c3;
take c10 = c6;
thus ( c1 = c9 & c2 = [0,c10] & c8 = c9 - c10 ) by E10, E12, 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
E10: c4 in {0} and
E11: c5 in REAL+ and
E12: c1 = [c4,c5] by ZFMISC_1:103;
reconsider c6 = c5 as Element of REAL+ by E11;
reconsider c7 = c3 - c6 as Element of REAL by E5;
take c8 = c7;
take c9 = c6;
take c10 = c3;
thus ( c1 = [0,c9] & c2 = c10 & c8 = c10 - c9 ) by E10, E12, TARSKI:def 1;
end;
( c1 in REAL+ \/ [:{0},REAL+ :] & c2 in REAL+ \/ [:{0},REAL+ :] ) by NUMBERS:def 1, XBOOLE_0:def 4;
then E10: ( ( c1 in REAL+ or c1 in [:{0},REAL+ :] ) & ( c2 in REAL+ or c2 in [:{0},REAL+ :] ) ) by XBOOLE_0:def 2;
assume E11: ( 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
E12: c3 in {0} and
E13: c4 in REAL+ and
E14: c1 = [c3,c4] by E10, ZFMISC_1:103;
reconsider c5 = c4 as Element of REAL+ by E13;
consider c6, c7 being set such that
E15: c6 in {0} and
E16: c7 in REAL+ and
E17: c2 = [c6,c7] by E10, E11, ZFMISC_1:103;
reconsider c8 = c7 as Element of REAL+ by E16;
c1 = [0,c5] by E12, E14, TARSKI:def 1;
then c5 <> 0 by E4;
then c5 + c8 <> 0 by ARYTM_2:6;
then reconsider c9 = [0,(c8 + c5)] as Element of REAL by E3;
take c9 ;
take c5 ;
take c8 ;
thus ( c1 = [0,c5] & c2 = [0,c8] & c9 = [0,(c5 + c8)] ) by E12, E14, E15, E17, 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 E10: ( c1 = [0,c5] & c2 = [0,c6] ) and
E11: c3 = [0,(c5 + c6)] ;
given c7, c8 being Element of REAL+ such that E12: ( c1 = [0,c7] & c2 = [0,c8] ) and
E13: c4 = [0,(c7 + c8)] ;
( c5 = c7 & c6 = c8 ) by E10, E12, ZFMISC_1:33;
hence c3 = c4 by E11, E13;
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 E6, 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 * c1,c2 -> Element of REAL means :E11: :: 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 E2;
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
E10: c4 in {0} and
E11: c5 in REAL+ and
E12: c2 = [c4,c5] by ZFMISC_1:103;
reconsider c6 = c5 as Element of REAL+ by E11;
assume E13: c1 <> 0 ;
c2 = [0,c6] by E10, E12, TARSKI:def 1;
then c6 <> 0 by E4;
then c3 *' c6 <> 0 by E13, ARYTM_1:2;
then reconsider c7 = [0,(c3 *' c6)] as Element of REAL by E3;
take c8 = c7;
take c9 = c3;
take c10 = c6;
thus ( c1 = c9 & c2 = [0,c10] & c8 = [0,(c9 *' c10)] ) by E10, E12, 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
E10: c4 in {0} and
E11: c5 in REAL+ and
E12: c1 = [c4,c5] by ZFMISC_1:103;
reconsider c6 = c5 as Element of REAL+ by E11;
assume E13: c2 <> 0 ;
c1 = [0,c6] by E10, E12, TARSKI:def 1;
then c6 <> 0 by E4;
then c6 *' c3 <> 0 by E13, ARYTM_1:2;
then reconsider c7 = [0,(c3 *' c6)] as Element of REAL by E3;
take c8 = c7;
take c9 = c6;
take c10 = c3;
thus ( c1 = [0,c9] & c2 = c10 & c8 = [0,(c10 *' c9)] ) by E10, E12, TARSKI:def 1;
end;
hereby
assume c1 in [:{0},REAL+ :] ;
then consider c3, c4 being set such that
E10: c3 in {0} and
E11: c4 in REAL+ and
E12: c1 = [c3,c4] by ZFMISC_1:103;
reconsider c5 = c4 as Element of REAL+ by E11;
assume c2 in [:{0},REAL+ :] ;
then consider c6, c7 being set such that
E13: c6 in {0} and
E14: c7 in REAL+ and
E15: c2 = [c6,c7] by ZFMISC_1:103;
reconsider c8 = c7 as Element of REAL+ by E14;
c5 *' c8 in REAL+ ;
then reconsider c9 = c8 *' c5 as Element of REAL by E2;
take c10 = c9;
take c11 = c5;
take c12 = c8;
thus ( c1 = [0,c11] & c2 = [0,c12] & c10 = c12 *' c11 ) by E10, E12, E13, E15, 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 E2, 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 E10: ( c1 = [0,c5] & c2 = [0,c6] ) and
E11: c3 = c6 *' c5 ;
given c7, c8 being Element of REAL+ such that E12: ( c1 = [0,c7] & c2 = [0,c8] ) and
E13: c4 = c8 *' c7 ;
( c5 = c7 & c6 = c8 ) by E10, E12, ZFMISC_1:33;
hence c3 = c4 by E11, E13;
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 = [0,b3] & b1 = [0,(b2 *' b3)] ) ) ) ) ) ) & ( ( c1 in REAL+ & c2 in [: