:: REALSET2 semantic presentation

begin

definition
func add_2  ->  BinOp of 2 equals :: REALSET2:def 1
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0);
coherence
 ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0) is BinOp of 2
proof
set f2 = ((0,0) .--> 0) +* ((0,1) .--> 1);
set f1 = (((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1);
set f = ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0);
A1: dom (((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0)) = (dom ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1))) \/ (dom ((1,1) .--> 0)) by FUNCT_4:def_1
.= (dom ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1))) \/ {[1,1]} by FUNCOP_1:13
.= ((dom (((0,0) .--> 0) +* ((0,1) .--> 1))) \/ (dom ((1,0) .--> 1))) \/ {[1,1]} by FUNCT_4:def_1
.= ((dom (((0,0) .--> 0) +* ((0,1) .--> 1))) \/ {[1,0]}) \/ {[1,1]} by FUNCOP_1:13
.= (((dom ((0,0) .--> 0)) \/ (dom ((0,1) .--> 1))) \/ {[1,0]}) \/ {[1,1]} by FUNCT_4:def_1
.= (((dom ((0,0) .--> 0)) \/ {[0,1]}) \/ {[1,0]}) \/ {[1,1]} by FUNCOP_1:13
.= (({[0,0]} \/ {[0,1]}) \/ {[1,0]}) \/ {[1,1]} by FUNCOP_1:13
.= ({[0,0],[0,1]} \/ {[1,0]}) \/ {[1,1]} by ENUMSET1:1
.= {[0,0],[0,1],[1,0]} \/ {[1,1]} by ENUMSET1:3
.= {[0,0],[0,1],[1,0],[1,1]} by ENUMSET1:6
.= [:2,2:] by CARD_1:50, ZFMISC_1:122 ;
A2: 1 c= 2 by CARD_1:49, CARD_1:50, ZFMISC_1:7;
 rng ((0,0) .--> 0) c= 1 by CARD_1:49, FUNCOP_1:13;
then A3: rng ((0,0) .--> 0) c= 2 by A2, XBOOLE_1:1;
A4: {1} c= 2 by CARD_1:50, ZFMISC_1:7;
 rng ((0,1) .--> 1) c= {1} by FUNCOP_1:13;
then  rng ((0,1) .--> 1) c= 2 by A4, XBOOLE_1:1;
then A5: (rng ((0,0) .--> 0)) \/ (rng ((0,1) .--> 1)) c= 2 by A3, XBOOLE_1:8;
 rng ((1,0) .--> 1) c= {1} by FUNCOP_1:13;
then A6: rng ((1,0) .--> 1) c= 2 by A4, XBOOLE_1:1;
 rng (((0,0) .--> 0) +* ((0,1) .--> 1)) c= (rng ((0,0) .--> 0)) \/ (rng ((0,1) .--> 1)) by FUNCT_4:17;
then  rng (((0,0) .--> 0) +* ((0,1) .--> 1)) c= 2 by A5, XBOOLE_1:1;
then A7: (rng (((0,0) .--> 0) +* ((0,1) .--> 1))) \/ (rng ((1,0) .--> 1)) c= 2 by A6, XBOOLE_1:8;
 rng ((1,1) .--> 0) c= 1 by CARD_1:49, FUNCOP_1:13;
then A8: rng ((1,1) .--> 0) c= 2 by A2, XBOOLE_1:1;
 rng ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) c= (rng (((0,0) .--> 0) +* ((0,1) .--> 1))) \/ (rng ((1,0) .--> 1)) by FUNCT_4:17;
then  rng ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) c= 2 by A7, XBOOLE_1:1;
then A9: (rng ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1))) \/ (rng ((1,1) .--> 0)) c= 2 by A8, XBOOLE_1:8;
 rng (((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0)) c= (rng ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1))) \/ (rng ((1,1) .--> 0)) by FUNCT_4:17;
then  rng (((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0)) c= 2 by A9, XBOOLE_1:1;
hence  ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0) is BinOp of 2 by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
func mult_2  ->  BinOp of 2 equals :: REALSET2:def 2
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1);
coherence
 ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1) is BinOp of 2
proof
A10: rng ((1,1) .--> 1) c= {1} by FUNCOP_1:13;
 {1} c= 2 by CARD_1:50, ZFMISC_1:7;
then A11: rng ((1,1) .--> 1) c= 2 by A10, XBOOLE_1:1;
set f2 = ((0,0) .--> 0) +* ((0,1) .--> 0);
set f1 = (((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0);
set f = ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1);
A12: dom (((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1)) = (dom ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0))) \/ (dom ((1,1) .--> 1)) by FUNCT_4:def_1
.= (dom ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0))) \/ {[1,1]} by FUNCOP_1:13
.= ((dom (((0,0) .--> 0) +* ((0,1) .--> 0))) \/ (dom ((1,0) .--> 0))) \/ {[1,1]} by FUNCT_4:def_1
.= ((dom (((0,0) .--> 0) +* ((0,1) .--> 0))) \/ {[1,0]}) \/ {[1,1]} by FUNCOP_1:13
.= (((dom ((0,0) .--> 0)) \/ (dom ((0,1) .--> 0))) \/ {[1,0]}) \/ {[1,1]} by FUNCT_4:def_1
.= (((dom ((0,0) .--> 0)) \/ {[0,1]}) \/ {[1,0]}) \/ {[1,1]} by FUNCOP_1:13
.= (({[0,0]} \/ {[0,1]}) \/ {[1,0]}) \/ {[1,1]} by FUNCOP_1:13
.= ({[0,0],[0,1]} \/ {[1,0]}) \/ {[1,1]} by ENUMSET1:1
.= {[0,0],[0,1],[1,0]} \/ {[1,1]} by ENUMSET1:3
.= {[0,0],[0,1],[1,0],[1,1]} by ENUMSET1:6
.= [:2,2:] by CARD_1:50, ZFMISC_1:122 ;
A13: 1 c= 2 by CARD_1:49, CARD_1:50, ZFMISC_1:7;
 rng ((0,0) .--> 0) c= 1 by CARD_1:49, FUNCOP_1:13;
then A14: rng ((0,0) .--> 0) c= 2 by A13, XBOOLE_1:1;
 rng ((0,1) .--> 0) c= 1 by CARD_1:49, FUNCOP_1:13;
then  rng ((0,1) .--> 0) c= 2 by A13, XBOOLE_1:1;
then A15: (rng ((0,0) .--> 0)) \/ (rng ((0,1) .--> 0)) c= 2 by A14, XBOOLE_1:8;
 rng ((1,0) .--> 0) c= 1 by CARD_1:49, FUNCOP_1:13;
then A16: rng ((1,0) .--> 0) c= 2 by A13, XBOOLE_1:1;
 rng (((0,0) .--> 0) +* ((0,1) .--> 0)) c= (rng ((0,0) .--> 0)) \/ (rng ((0,1) .--> 0)) by FUNCT_4:17;
then  rng (((0,0) .--> 0) +* ((0,1) .--> 0)) c= 2 by A15, XBOOLE_1:1;
then A17: (rng (((0,0) .--> 0) +* ((0,1) .--> 0))) \/ (rng ((1,0) .--> 0)) c= 2 by A16, XBOOLE_1:8;
 rng ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) c= (rng (((0,0) .--> 0) +* ((0,1) .--> 0))) \/ (rng ((1,0) .--> 0)) by FUNCT_4:17;
then  rng ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) c= 2 by A17, XBOOLE_1:1;
then A18: (rng ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0))) \/ (rng ((1,1) .--> 1)) c= 2 by A11, XBOOLE_1:8;
 rng (((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1)) c= (rng ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0))) \/ (rng ((1,1) .--> 1)) by FUNCT_4:17;
then  rng (((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1)) c= 2 by A18, XBOOLE_1:1;
hence  ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1) is BinOp of 2 by A12, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;

:: deftheorem  defines add_2 REALSET2:def_1_:_
 add_2 = ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0);

:: deftheorem  defines mult_2 REALSET2:def_2_:_
 mult_2 = ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1);

  set x = In (0,2);

set y = In (1,2);

Lm1:  1 in 2
by CARD_1:50, TARSKI:def_2;

Lm2:  0 in 2
by CARD_1:50, TARSKI:def_2;

then Lm3:  In (0,2) = 0
by FUNCT_7:def_1;

Lm4:  In (1,2) = 1
by Lm1, FUNCT_7:def_1;

set Z = 2;

reconsider A = 2 as non trivial set by Lm1, Lm2, ZFMISC_1:def_10;

reconsider nd = In (0,2) as Element of A ;

Lm5:  dom ((1,1) .--> 0) = {[1,1]}
by FUNCOP_1:13;

Lm6:  dom ((1,0) .--> 1) = {[1,0]}
by FUNCOP_1:13;

Lm7:  dom ((0,1) .--> 1) = {[0,1]}
by FUNCOP_1:13;

Lm8:  add_2 . ((In (0,2)),(In (0,2))) = In (0,2)
proof
 [(In (0,2)),(In (0,2))] <> [0,1] by Lm3, XTUPLE_0:1;
then A1: not [(In (0,2)),(In (0,2))] in dom ((0,1) .--> 1) by Lm7, TARSKI:def_1;
 [(In (0,2)),(In (0,2))] <> [1,0] by Lm3, XTUPLE_0:1;
then A2: not [(In (0,2)),(In (0,2))] in dom ((1,0) .--> 1) by Lm6, TARSKI:def_1;
 [(In (0,2)),(In (0,2))] <> [1,1] by Lm3, XTUPLE_0:1;
then  not [(In (0,2)),(In (0,2))] in dom ((1,1) .--> 0) by Lm5, TARSKI:def_1;
hence add_2 . ((In (0,2)),(In (0,2))) = ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . ((In (0,2)),(In (0,2))) by FUNCT_4:11
.= (((0,0) .--> 0) +* ((0,1) .--> 1)) . ((In (0,2)),(In (0,2))) by A2, FUNCT_4:11
.= ((0,0) .--> 0) . ((In (0,2)),(In (0,2))) by A1, FUNCT_4:11
.= In (0,2) by Lm3, FUNCOP_1:71 ;
::_thesis: verum
end;

Lm9:  add_2 . ((In (0,2)),(In (1,2))) = In (1,2)
proof
 [(In (0,2)),(In (1,2))] <> [1,0] by Lm3, XTUPLE_0:1;
then A1: not [(In (0,2)),(In (1,2))] in dom ((1,0) .--> 1) by Lm6, TARSKI:def_1;
A2: [(In (0,2)),(In (1,2))] in dom ((0,1) .--> 1) by Lm3, Lm4, Lm7, TARSKI:def_1;
 [(In (0,2)),(In (1,2))] <> [1,1] by Lm3, XTUPLE_0:1;
then  not [(In (0,2)),(In (1,2))] in dom ((1,1) .--> 0) by Lm5, TARSKI:def_1;
hence add_2 . ((In (0,2)),(In (1,2))) = ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . ((In (0,2)),(In (1,2))) by FUNCT_4:11
.= (((0,0) .--> 0) +* ((0,1) .--> 1)) . ((In (0,2)),(In (1,2))) by A1, FUNCT_4:11
.= ((0,1) .--> 1) . ((In (0,2)),(In (1,2))) by A2, FUNCT_4:13
.= In (1,2) by Lm3, Lm4, FUNCOP_1:71 ;
::_thesis: verum
end;

Lm10:  add_2 . ((In (1,2)),(In (0,2))) = In (1,2)
proof
A1: [(In (1,2)),(In (0,2))] in dom ((1,0) .--> 1) by Lm3, Lm4, Lm6, TARSKI:def_1;
 [(In (1,2)),(In (0,2))] <> [1,1] by Lm3, XTUPLE_0:1;
then  not [(In (1,2)),(In (0,2))] in dom ((1,1) .--> 0) by Lm5, TARSKI:def_1;
hence add_2 . ((In (1,2)),(In (0,2))) = ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . ((In (1,2)),(In (0,2))) by FUNCT_4:11
.= ((1,0) .--> 1) . ((In (1,2)),(In (0,2))) by A1, FUNCT_4:13
.= In (1,2) by Lm3, Lm4, FUNCOP_1:71 ;
::_thesis: verum
end;

Lm11:  add_2 . ((In (1,2)),(In (1,2))) = In (0,2)
proof
 [(In (1,2)),(In (1,2))] in dom ((1,1) .--> 0) by Lm4, Lm5, TARSKI:def_1;
hence add_2 . ((In (1,2)),(In (1,2))) = ((1,1) .--> 0) . ((In (1,2)),(In (1,2))) by FUNCT_4:13
.= In (0,2) by Lm3, Lm4, FUNCOP_1:71 ;
::_thesis: verum
end;

Lm12:  dom ((1,1) .--> 1) = {[1,1]}
by FUNCOP_1:13;

Lm13:  dom ((1,0) .--> 0) = {[1,0]}
by FUNCOP_1:13;

Lm14:  dom ((0,1) .--> 0) = {[0,1]}
by FUNCOP_1:13;

Lm15:  mult_2 . ((In (0,2)),(In (0,2))) = In (0,2)
proof
 [(In (0,2)),(In (0,2))] <> [0,1] by Lm3, XTUPLE_0:1;
then A1: not [(In (0,2)),(In (0,2))] in dom ((0,1) .--> 0) by Lm14, TARSKI:def_1;
 [(In (0,2)),(In (0,2))] <> [1,0] by Lm3, XTUPLE_0:1;
then A2: not [(In (0,2)),(In (0,2))] in dom ((1,0) .--> 0) by Lm13, TARSKI:def_1;
 [(In (0,2)),(In (0,2))] <> [1,1] by Lm3, XTUPLE_0:1;
then  not [(In (0,2)),(In (0,2))] in dom ((1,1) .--> 1) by Lm12, TARSKI:def_1;
hence mult_2 . ((In (0,2)),(In (0,2))) = ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . ((In (0,2)),(In (0,2))) by FUNCT_4:11
.= (((0,0) .--> 0) +* ((0,1) .--> 0)) . ((In (0,2)),(In (0,2))) by A2, FUNCT_4:11
.= ((0,0) .--> 0) . ((In (0,2)),(In (0,2))) by A1, FUNCT_4:11
.= In (0,2) by Lm3, FUNCOP_1:71 ;
::_thesis: verum
end;

Lm16:  mult_2 . ((In (0,2)),(In (1,2))) = In (0,2)
proof
 [(In (0,2)),(In (1,2))] <> [1,0] by Lm3, XTUPLE_0:1;
then A1: not [(In (0,2)),(In (1,2))] in dom ((1,0) .--> 0) by Lm13, TARSKI:def_1;
A2: [(In (0,2)),(In (1,2))] in dom ((0,1) .--> 0) by Lm3, Lm4, Lm14, TARSKI:def_1;
 [(In (0,2)),(In (1,2))] <> [1,1] by Lm3, XTUPLE_0:1;
then  not [(In (0,2)),(In (1,2))] in dom ((1,1) .--> 1) by Lm12, TARSKI:def_1;
hence mult_2 . ((In (0,2)),(In (1,2))) = ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . ((In (0,2)),(In (1,2))) by FUNCT_4:11
.= (((0,0) .--> 0) +* ((0,1) .--> 0)) . ((In (0,2)),(In (1,2))) by A1, FUNCT_4:11
.= ((0,1) .--> 0) . ((In (0,2)),(In (1,2))) by A2, FUNCT_4:13
.= In (0,2) by Lm3, Lm4, FUNCOP_1:71 ;
::_thesis: verum
end;

Lm17:  mult_2 . ((In (1,2)),(In (0,2))) = In (0,2)
proof
A1: [(In (1,2)),(In (0,2))] in dom ((1,0) .--> 0) by Lm3, Lm4, Lm13, TARSKI:def_1;
 [(In (1,2)),(In (0,2))] <> [1,1] by Lm3, XTUPLE_0:1;
then  not [(In (1,2)),(In (0,2))] in dom ((1,1) .--> 1) by Lm12, TARSKI:def_1;
hence mult_2 . ((In (1,2)),(In (0,2))) = ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . ((In (1,2)),(In (0,2))) by FUNCT_4:11
.= ((1,0) .--> 0) . ((In (1,2)),(In (0,2))) by A1, FUNCT_4:13
.= In (0,2) by Lm3, Lm4, FUNCOP_1:71 ;
::_thesis: verum
end;

Lm18:  mult_2 . ((In (1,2)),(In (1,2))) = In (1,2)
proof
 [(In (1,2)),(In (1,2))] in dom ((1,1) .--> 1) by Lm4, Lm12, TARSKI:def_1;
hence mult_2 . ((In (1,2)),(In (1,2))) = ((1,1) .--> 1) . ((In (1,2)),(In (1,2))) by FUNCT_4:13
.= In (1,2) by Lm4, FUNCOP_1:71 ;
::_thesis: verum
end;

set om = mult_2 ;

Lm19:  A \ {(In (0,2))} = {(In (1,2))}
by Lm3, Lm4, CARD_1:50, ZFMISC_1:17;

then Lm20:  [:(A \ {(In (0,2))}),(A \ {(In (0,2))}):] = {[(In (1,2)),(In (1,2))]}
by ZFMISC_1:29;

Lm21:  for t being set st t in [:(A \ {(In (0,2))}),(A \ {(In (0,2))}):] holds
mult_2 . t in A \ {(In (0,2))}
proof
let t be set ; ::_thesis: ( t in [:(A \ {(In (0,2))}),(A \ {(In (0,2))}):] implies mult_2 . t in A \ {(In (0,2))} )
assume  t in [:(A \ {(In (0,2))}),(A \ {(In (0,2))}):] ; ::_thesis: mult_2 . t in A \ {(In (0,2))}
then  t = [(In (1,2)),(In (1,2))] by Lm20, TARSKI:def_1;
hence  mult_2 . t in A \ {(In (0,2))} by Lm18, Lm19, TARSKI:def_1; ::_thesis: verum
end;

reconsider nm = In (1,2) as Element of A \ {nd} by Lm19, TARSKI:def_1;

reconsider od0 = add_2 as BinOp of A ;

reconsider om0 = mult_2 as BinOp of A ;

Lm22:  for a, b, d being Element of A holds add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))
proof
let a, b, d be Element of A; ::_thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))
A1: ( a = In (0,2) or a = In (1,2) ) by Lm3, Lm4, CARD_1:50, TARSKI:def_2;
A2: ( b = In (0,2) or b = In (1,2) ) by Lm3, Lm4, CARD_1:50, TARSKI:def_2;
A3: ( d = In (0,2) or d = In (1,2) ) by Lm3, Lm4, CARD_1:50, TARSKI:def_2;
percases ( a = In (0,2) or b = In (0,2) or d = In (0,2) or ( a = In (1,2) & b = In (1,2) & d = In (1,2) ) ) by Lm3, Lm4, CARD_1:50, TARSKI:def_2;
suppose a = In (0,2) ; ::_thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))
hence  add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d))) by A2, A3, Lm8, Lm9, Lm10, Lm11; ::_thesis: verum
end;
suppose b = In (0,2) ; ::_thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))
hence  add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d))) by A1, A3, Lm8, Lm9, Lm10; ::_thesis: verum
end;
suppose d = In (0,2) ; ::_thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))
hence  add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d))) by A1, A2, Lm8, Lm9, Lm10, Lm11; ::_thesis: verum
end;
suppose ( a = In (1,2) & b = In (1,2) & d = In (1,2) ) ; ::_thesis: add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))
hence  add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d))) by Lm9, Lm10, Lm11; ::_thesis: verum
end;
end;
end;

reconsider dL = doubleLoopStr(# A,od0,om0,nm,nd #) as non empty doubleLoopStr ;

Lm23:  for a being Element of dL holds a + (0. dL) = a
proof
let a be Element of dL; ::_thesis: a + (0. dL) = a
 ( a = In (0,2) or a = In (1,2) ) by Lm3, Lm4, CARD_1:50, TARSKI:def_2;
hence  a + (0. dL) = a by Lm8, Lm10; ::_thesis: verum
end;

Lm24:  for a, b, c being Element of dL holds (a + b) + c = a + (b + c)
by Lm22;

Lm25:  for a, b being Element of dL holds a + b = b + a
proof
let a, b be Element of dL; ::_thesis: a + b = b + a
 ( ( a = In (0,2) & b = In (0,2) ) or ( a = In (0,2) & b = In (1,2) ) or ( a = In (1,2) & b = In (0,2) ) or ( a = In (1,2) & b = In (1,2) ) ) by Lm3, Lm4, CARD_1:50, TARSKI:def_2;
hence  a + b = b + a by Lm9, Lm10; ::_thesis: verum
end;

reconsider om1 = mult_2 as DnT of nd,A by Lm21, REALSET1:def_6;

Lm26:  for B being non empty set
for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm holds
addLoopStr(# B,P,e #) is AbGroup
proof
let B be non empty set ; ::_thesis: for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm holds
addLoopStr(# B,P,e #) is AbGroup
let P be BinOp of B; ::_thesis: for e being Element of B st B = A \ {nd} & e = nm holds
addLoopStr(# B,P,e #) is AbGroup
let e be Element of B; ::_thesis: ( B = A \ {nd} & e = nm implies addLoopStr(# B,P,e #) is AbGroup )
assume that
A1: B = A \ {nd} and
A2: e = nm ; ::_thesis: addLoopStr(# B,P,e #) is AbGroup
A3: addLoopStr(# B,P,e #) is right_complementable
proof
let a be Element of addLoopStr(# B,P,e #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
take  a ; :: according to ALGSTR_0:def_11 ::_thesis: a + a = 0. addLoopStr(# B,P,e #)
thus  a + a = 0. addLoopStr(# B,P,e #) by A1, A2, Lm19, TARSKI:def_1; ::_thesis: verum
end;
 for a, b, c being Element of B holds P . ((P . (a,b)),c) = P . (a,(P . (b,c)))
proof
let a, b, c be Element of B; ::_thesis: P . ((P . (a,b)),c) = P . (a,(P . (b,c)))
A4: b = In (1,2) by A1, Lm19, TARSKI:def_1;
A5: c = In (1,2) by A1, Lm19, TARSKI:def_1;
 a = In (1,2) by A1, Lm19, TARSKI:def_1;
hence  P . ((P . (a,b)),c) = P . (a,(P . (b,c))) by A1, A4, A5, Lm19, TARSKI:def_1; ::_thesis: verum
end;
then A6: for a, b, c being Element of addLoopStr(# B,P,e #) holds (a + b) + c = a + (b + c) ;
A7: for a, b being Element of addLoopStr(# B,P,e #) holds a + b = b + a
proof
let a, b be Element of addLoopStr(# B,P,e #); ::_thesis: a + b = b + a
 a = In (1,2) by A1, Lm19, TARSKI:def_1;
hence  a + b = b + a by A1, Lm19, TARSKI:def_1; ::_thesis: verum
end;
 for a being Element of addLoopStr(# B,P,e #) holds a + (0. addLoopStr(# B,P,e #)) = a
proof
let a be Element of addLoopStr(# B,P,e #); ::_thesis: a + (0. addLoopStr(# B,P,e #)) = a
 a = In (1,2) by A1, Lm19, TARSKI:def_1;
hence  a + (0. addLoopStr(# B,P,e #)) = a by A1, Lm19, TARSKI:def_1; ::_thesis: verum
end;
hence  addLoopStr(# B,P,e #) is AbGroup by A3, A6, A7, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
end;

Lm27:  for a, b, d being Element of dL holds
( a * (b + d) = (a * b) + (a * d) & (b + d) * a = (b * a) + (d * a) )
proof
let a, b, d be Element of dL; ::_thesis: ( a * (b + d) = (a * b) + (a * d) & (b + d) * a = (b * a) + (d * a) )
A1: ( ( a = In (0,2) & b = In (0,2) & d = In (0,2) ) or ( a = In (0,2) & b = In (0,2) & d = In (1,2) ) or ( a = In (0,2) & b = In (1,2) & d = In (0,2) ) or ( a = In (0,2) & b = In (1,2) & d = In (1,2) ) or ( a = In (1,2) & b = In (0,2) & d = In (0,2) ) or ( a = In (1,2) & b = In (0,2) & d = In (1,2) ) or ( a = In (1,2) & b = In (1,2) & d = In (0,2) ) or ( a = In (1,2) & b = In (1,2) & d = In (1,2) ) ) by Lm3, Lm4, CARD_1:50, TARSKI:def_2;
hence  a * (b + d) = (a * b) + (a * d) by Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18; ::_thesis: (b + d) * a = (b * a) + (d * a)
thus  (b + d) * a = (b * a) + (d * a) by A1, Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18; ::_thesis: verum
end;

definition
func dL-Z_2  ->  doubleLoopStr  equals :: REALSET2:def 3
 doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #);
coherence
 doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #) is doubleLoopStr ;
end;

:: deftheorem  defines dL-Z_2 REALSET2:def_3_:_
 dL-Z_2 = doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #);

registration
cluster dL-Z_2  ->  non empty non degenerated strict ;
coherence
 ( dL-Z_2 is strict & not dL-Z_2 is empty & not dL-Z_2 is degenerated )
proof
thus  dL-Z_2 is strict ; ::_thesis: ( not dL-Z_2 is empty & not dL-Z_2 is degenerated )
thus  not the carrier of dL-Z_2 is empty ; :: according to STRUCT_0:def_1 ::_thesis: not dL-Z_2 is degenerated
 0 in 2 by CARD_1:50, TARSKI:def_2;
then A1: 0. dL-Z_2 = 0 by FUNCT_7:def_1;
 1 in 2 by CARD_1:50, TARSKI:def_2;
hence  0. dL-Z_2 <> 1. dL-Z_2 by A1, FUNCT_7:def_1; :: according to STRUCT_0:def_8 ::_thesis: verum
end;
end;

registration
cluster dL-Z_2  ->  add-associative distributive ;
coherence
 ( dL-Z_2 is add-associative & dL-Z_2 is distributive )
proof
 for a, b, c being Element of dL-Z_2 holds (a + b) + c = a + (b + c) by Lm22;
hence  dL-Z_2 is add-associative by RLVECT_1:def_3; ::_thesis: dL-Z_2 is distributive
thus  dL-Z_2 is distributive ::_thesis: verum
proof
let a, b, d be Element of dL-Z_2; :: according to VECTSP_1:def_7 ::_thesis: ( a * (b + d) = (a * b) + (a * d) & (b + d) * a = (b * a) + (d * a) )
A1: ( ( a = In (0,2) & b = In (0,2) & d = In (0,2) ) or ( a = In (0,2) & b = In (0,2) & d = In (1,2) ) or ( a = In (0,2) & b = In (1,2) & d = In (0,2) ) or ( a = In (0,2) & b = In (1,2) & d = In (1,2) ) or ( a = In (1,2) & b = In (0,2) & d = In (0,2) ) or ( a = In (1,2) & b = In (0,2) & d = In (1,2) ) or ( a = In (1,2) & b = In (1,2) & d = In (0,2) ) or ( a = In (1,2) & b = In (1,2) & d = In (1,2) ) ) by Lm3, Lm4, CARD_1:50, TARSKI:def_2;
hence  a * (b + d) = (a * b) + (a * d) by Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18; ::_thesis: (b + d) * a = (b * a) + (d * a)
thus  (b + d) * a = (b * a) + (d * a) by A1, Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18; ::_thesis: verum
end;
end;
end;

registration
cluster non empty non trivial strict add-associative for doubleLoopStr ;
existence
 ex b1 being non trivial strict doubleLoopStr st b1 is add-associative
proof
take  dL-Z_2 ; ::_thesis: dL-Z_2 is add-associative
thus  dL-Z_2 is add-associative ; ::_thesis: verum
end;
end;

registration
cluster the carrier of dL-Z_2 ->  natural-membered ;
coherence
 the carrier of dL-Z_2 is natural-membered
proof
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( not x in the carrier of dL-Z_2 or not x is V27() )
thus  ( not x in the carrier of dL-Z_2 or not x is V27() ) by CARD_1:50, TARSKI:def_2; ::_thesis: verum
end;
end;

registration
cluster empty for Element of the carrier of dL-Z_2;
existence
 ex b1 being Element of dL-Z_2 st b1 is empty
proof
reconsider z = 0 as Element of dL-Z_2 by CARD_1:50, TARSKI:def_2;
take  z ; ::_thesis: z is empty
thus  z is empty ; ::_thesis: verum
end;
cluster non empty for Element of the carrier of dL-Z_2;
existence
 not for b1 being Element of dL-Z_2 holds b1 is empty
proof
reconsider z = 1 as Element of dL-Z_2 by CARD_1:50, TARSKI:def_2;
take  z ; ::_thesis: not z is empty
thus  not z is empty ; ::_thesis: verum
end;
end;

definition
let L be doubleLoopStr ;
attrL is Field-like  means :Def4: :: REALSET2:def 4
( the multF of L is DnT of 0. L, the carrier of L & ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup ) );
end;

:: deftheorem Def4 defines Field-like REALSET2:def_4_:_
 for L being doubleLoopStr holds
( L is Field-like iff ( the multF of L is DnT of 0. L, the carrier of L & ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup ) ) );

registration
let A be non empty set ;
let od be BinOp of A;
let nd be Element of A;
let om be BinOp of A;
let nm be Element of A;
cluster doubleLoopStr(# A,od,om,nm,nd #) ->  non empty ;
coherence
 not doubleLoopStr(# A,od,om,nm,nd #) is empty ;
end;

Lm28:  for B being non empty set
for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm & P = om1 ! (A,nd) holds
addLoopStr(# B,P,e #) is AbGroup
by Lm26;

registration
cluster non empty non degenerated non trivial right_complementable strict Abelian add-associative right_zeroed distributive Field-like for doubleLoopStr ;
existence
 ex b1 being non degenerated doubleLoopStr st
( b1 is strict & b1 is Field-like & b1 is Abelian & b1 is distributive & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proof
set L = doubleLoopStr(# A,od0,om0,nm,nd #);
A1: 0. doubleLoopStr(# A,od0,om0,nm,nd #) = nd ;
 1. doubleLoopStr(# A,od0,om0,nm,nd #) = nm ;
then reconsider L = doubleLoopStr(# A,od0,om0,nm,nd #) as non degenerated doubleLoopStr by A1, Lm3, Lm4, STRUCT_0:def_8;
take  L ; ::_thesis: ( L is strict & L is Field-like & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable )
thus  L is strict ; ::_thesis: ( L is Field-like & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable )
thus  the multF of L is DnT of 0. L, the carrier of L by Lm28; :: according to REALSET2:def_4 ::_thesis: ( ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup ) & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable )
 L is right_complementable
proof
let a be Element of L; :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
take  a ; :: according to ALGSTR_0:def_11 ::_thesis: a + a = 0. L
 ( a = In (0,2) or a = In (1,2) ) by Lm3, Lm4, CARD_1:50, TARSKI:def_2;
hence  a + a = 0. L by Lm8, Lm11; ::_thesis: verum
end;
hence  ( ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup ) & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable ) by Lm23, Lm24, Lm25, Lm26, Lm27, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, VECTSP_1:def_7; ::_thesis: verum
end;
end;

registration
cluster non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive  ->  non degenerated Field-like for doubleLoopStr ;
coherence
 for b1 being non degenerated doubleLoopStr st b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is well-unital & b1 is distributive & b1 is almost_left_invertible holds
b1 is Field-like
proof
let L be non degenerated doubleLoopStr ; ::_thesis: ( L is add-associative & L is right_zeroed & L is right_complementable & L is Abelian & L is commutative & L is associative & L is well-unital & L is distributive & L is almost_left_invertible implies L is Field-like )
set B = NonZero L;
assume A1: ( L is add-associative & L is right_zeroed & L is right_complementable & L is Abelian & L is commutative & L is associative & L is well-unital & L is distributive & L is almost_left_invertible ) ; ::_thesis: L is Field-like
A2: for y being set st y in [:(NonZero L),(NonZero L):] holds
the multF of L . y in NonZero L
proof
let z be set ; ::_thesis: ( z in [:(NonZero L),(NonZero L):] implies the multF of L . z in NonZero L )
assume  z in [:(NonZero L),(NonZero L):] ; ::_thesis: the multF of L . z in NonZero L
then consider x, y being set  such that
A3: x in NonZero L and
A4: y in NonZero L and
A5: z = [x,y] by ZFMISC_1:84;
reconsider x = x, y = y as Element of L by A3, A4;
 not y in {(0. L)} by A4, XBOOLE_0:def_5;
then A6: y <> 0. L by TARSKI:def_1;
 not x in {(0. L)} by A3, XBOOLE_0:def_5;
then  x <> 0. L by TARSKI:def_1;
then  x * y <> 0. L by A1, A6, VECTSP_1:12;
then  not x * y in {(0. L)} by TARSKI:def_1;
hence  the multF of L . z in NonZero L by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  the multF of L is DnT of 0. L, the carrier of L by REALSET1:def_6; :: according to REALSET2:def_4 ::_thesis: for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup
reconsider om = the multF of L as DnT of 0. L, the carrier of L by A2, REALSET1:def_6;
let B be non empty set ; ::_thesis: for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup
let P be BinOp of B; ::_thesis: for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup
let e be Element of B; ::_thesis: ( B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) implies addLoopStr(# B,P,e #) is AbGroup )
assume that
A7: B = NonZero L and
A8: e = 1. L and
A9: P = the multF of L || (NonZero L) ; ::_thesis: addLoopStr(# B,P,e #) is AbGroup
set K = addLoopStr(# B,P,e #);
A10: addLoopStr(# B,P,e #) is Abelian
proof
let v, w be Element of addLoopStr(# B,P,e #); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider a = v, b = w as Element of L by A7, XBOOLE_0:def_5;
A11: [w,v] in [:B,B:] ;
 [v,w] in [:B,B:] ;
hence v + w = a * b by A7, A9, FUNCT_1:49
.= b * a by A1, GROUP_1:def_12
.= w + v by A7, A9, A11, FUNCT_1:49 ;
::_thesis: verum
end;
A12: addLoopStr(# B,P,e #) is right_complementable
proof
let v be Element of addLoopStr(# B,P,e #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider a = v as Element of L by A7, XBOOLE_0:def_5;
 not a in {(0. L)} by A7, XBOOLE_0:def_5;
then  a <> 0. L by TARSKI:def_1;
then consider b being Element of L such that
A13: b * a = 1. L by A1, VECTSP_1:def_9;
A14: a * b = 1. L by A1, A13, GROUP_1:def_12;
then  b <> 0. L by A1, VECTSP_1:6;
then  not b in {(0. L)} by TARSKI:def_1;
then reconsider w = b as Element of addLoopStr(# B,P,e #) by A7, XBOOLE_0:def_5;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. addLoopStr(# B,P,e #)
 [v,w] in [:B,B:] ;
hence  v + w = 0. addLoopStr(# B,P,e #) by A7, A8, A9, A14, FUNCT_1:49; ::_thesis: verum
end;
A15: addLoopStr(# B,P,e #) is add-associative
proof
let u, v, w be Element of addLoopStr(# B,P,e #); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
reconsider a = u, b = v, c = w as Element of L by A7, XBOOLE_0:def_5;
A16: [v,w] in [:B,B:] ;
then  P . (v,w) in B by FUNCT_2:5;
then A17: [u,((om || B) . (v,w))] in [:B,B:] by A7, A9, ZFMISC_1:87;
A18: [u,v] in [:B,B:] ;
then  P . (u,v) in B by FUNCT_2:5;
then  [((om || B) . (u,v)),w] in [:B,B:] by A7, A9, ZFMISC_1:87;
hence (u + v) + w = om . (((om || B) . (u,v)),w) by A7, A9, FUNCT_1:49
.= (a * b) * c by A18, FUNCT_1:49
.= a * (b * c) by A1, GROUP_1:def_3
.= om . (u,((om || B) . (v,w))) by A16, FUNCT_1:49
.= u + (v + w) by A7, A9, A17, FUNCT_1:49 ;
::_thesis: verum
end;
 addLoopStr(# B,P,e #) is right_zeroed
proof
let v be Element of addLoopStr(# B,P,e #); :: according to RLVECT_1:def_4 ::_thesis: v + (0. addLoopStr(# B,P,e #)) = v
reconsider a = v as Element of L by A7, XBOOLE_0:def_5;
 [v,(0. addLoopStr(# B,P,e #))] in [:B,B:] ;
hence v + (0. addLoopStr(# B,P,e #)) = a * (1. L) by A7, A8, A9, FUNCT_1:49
.= v by A1, VECTSP_1:def_6 ;
::_thesis: verum
end;
hence  addLoopStr(# B,P,e #) is AbGroup by A10, A15, A12; ::_thesis: verum
end;
end;

deffunc H1( non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ) ->  set = the carrier of $1;

definition
let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ;
func omf F ->  DnT of 0. F, the carrier of F equals :: REALSET2:def 5
 the multF of F;
coherence
 the multF of F is DnT of 0. F, the carrier of F by Def4;
end;

:: deftheorem  defines omf REALSET2:def_5_:_
 for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr holds omf F = the multF of F;

theorem :: REALSET2:1
for F being Field holds addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) is AbGroup
proof
let F be Field; ::_thesis: addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) is AbGroup
set L = addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #);
A1: addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) is add-associative
proof
let u, v, w be Element of addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
reconsider a = u, b = v, c = w as Element of F ;
thus (u + v) + w = (a + b) + c
.= a + (b + c) by RLVECT_1:def_3
.= u + (v + w) ; ::_thesis: verum
end;
A2: addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) is right_zeroed
proof
let v be Element of addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #); :: according to RLVECT_1:def_4 ::_thesis: v + (0. addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #)) = v
reconsider a = v as Element of F ;
thus v + (0. addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #)) = a + (0. F)
.= v by RLVECT_1:def_4 ; ::_thesis: verum
end;
A3: addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) is right_complementable
proof
let v be Element of addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider a = v as Element of F ;
consider b being Element of F such that
A4: a + b = 0. F by ALGSTR_0:def_11;
reconsider w = b as Element of addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #)
thus  v + w = 0. addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) by A4; ::_thesis: verum
end;
 addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) is Abelian
proof
let v, w be Element of addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider a = v, b = w as Element of F ;
thus v + w = a + b
.= b + a
.= w + v ; ::_thesis: verum
end;
hence  addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) is AbGroup by A1, A2, A3; ::_thesis: verum
end;

theorem :: REALSET2:2
for F being Field
for a being Element of F holds
( a + (0. F) = a & (0. F) + a = a ) by RLVECT_1:def_13;

theorem Th3: :: REALSET2:3
for F being AbGroup
for a being Element of F ex b being Element of F st
( a + b = 0. F & b + a = 0. F )
proof
let F be AbGroup; ::_thesis: for a being Element of F ex b being Element of F st
( a + b = 0. F & b + a = 0. F )
let a be Element of F; ::_thesis: ex b being Element of F st
( a + b = 0. F & b + a = 0. F )
consider b being Element of F such that
A1: a + b = 0. F by ALGSTR_0:def_11;
take  b ; ::_thesis: ( a + b = 0. F & b + a = 0. F )
thus  a + b = 0. F by A1; ::_thesis: b + a = 0. F
thus  b + a = 0. F by A1; ::_thesis: verum
end;

theorem Th4: :: REALSET2:4
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b, c being Element of NonZero F holds (a * b) * c = a * (b * c)
proof
let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; ::_thesis: for a, b, c being Element of NonZero F holds (a * b) * c = a * (b * c)
let a, b, c be Element of NonZero F; ::_thesis: (a * b) * c = a * (b * c)
set B = H1(F) \ {(0. F)};
set P = (omf F) ! (H1(F),(0. F));
A1: H1(F) \ {(0. F)} = NonZero F ;
then reconsider e = 1. F as Element of H1(F) \ {(0. F)} by STRUCT_0:2;
reconsider D = addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! (H1(F),(0. F))),e #) as strict AbGroup by A1, Def4;
reconsider a = a, b = b, c = c as Element of D ;
reconsider x = a, y = b, z = c as Element of F ;
A2: (omf F) || (H1(F) \ {(0. F)}) is Function of [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):],(H1(F) \ {(0. F)}) by REALSET1:7;
then A3: dom ((omf F) || (H1(F) \ {(0. F)})) = [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] by FUNCT_2:def_1;
A4: for x, y being Element of H1(F) \ {(0. F)} holds (omf F) . (x,y) = the addF of D . (x,y)
proof
let x, y be Element of H1(F) \ {(0. F)}; ::_thesis: (omf F) . (x,y) = the addF of D . (x,y)
 [x,y] in [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] ;
hence  (omf F) . (x,y) = the addF of D . (x,y) by A3, FUNCT_1:47; ::_thesis: verum
end;
A5: for s, t being Element of H1(F) \ {(0. F)} holds
( the addF of D . (s,t) is Element of H1(F) \ {(0. F)} & (omf F) . (s,t) is Element of H1(F) \ {(0. F)} )
proof
let s, t be Element of H1(F) \ {(0. F)}; ::_thesis: ( the addF of D . (s,t) is Element of H1(F) \ {(0. F)} & (omf F) . (s,t) is Element of H1(F) \ {(0. F)} )
A6: [s,t] in [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] ;
consider W being Function of [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):],(H1(F) \ {(0. F)}) such that
A7: W = (omf F) || (H1(F) \ {(0. F)}) by A2;
 W . (s,t) is Element of H1(F) \ {(0. F)} ;
hence  ( the addF of D . (s,t) is Element of H1(F) \ {(0. F)} & (omf F) . (s,t) is Element of H1(F) \ {(0. F)} ) by A3, A6, A7, FUNCT_1:47; ::_thesis: verum
end;
A8: for x, y, z being Element of H1(F) \ {(0. F)} holds
( (omf F) . (( the addF of D . (x,y)),z) = the addF of D . (( the addF of D . (x,y)),z) & the addF of D . (x,((omf F) . (y,z))) = (omf F) . (x,((omf F) . (y,z))) )
proof
let x, y, z be Element of H1(F) \ {(0. F)}; ::_thesis: ( (omf F) . (( the addF of D . (x,y)),z) = the addF of D . (( the addF of D . (x,y)),z) & the addF of D . (x,((omf F) . (y,z))) = (omf F) . (x,((omf F) . (y,z))) )
A9: (omf F) . (y,z) is Element of H1(F) \ {(0. F)} by A5;
 the addF of D . (x,y) is Element of H1(F) \ {(0. F)} by A5;
hence  ( (omf F) . (( the addF of D . (x,y)),z) = the addF of D . (( the addF of D . (x,y)),z) & the addF of D . (x,((omf F) . (y,z))) = (omf F) . (x,((omf F) . (y,z))) ) by A4, A9; ::_thesis: verum
end;
(x * y) * z = (omf F) . (( the addF of D . (a,b)),c) by A4
.= (a + b) + c by A8
.= a + (b + c) by RLVECT_1:def_3
.= the addF of D . (a,((omf F) . (b,c))) by A4
.= x * (y * z) by A8 ;
hence  (a * b) * c = a * (b * c) ; ::_thesis: verum
end;

theorem Th5: :: REALSET2:5
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b being Element of NonZero F holds a * b = b * a
proof
let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; ::_thesis: for a, b being Element of NonZero F holds a * b = b * a
let a, b be Element of NonZero F; ::_thesis: a * b = b * a
set B = H1(F) \ {(0. F)};
set P = (omf F) ! (H1(F),(0. F));
A1: H1(F) \ {(0. F)} = NonZero F ;
then reconsider e = 1. F as Element of H1(F) \ {(0. F)} by STRUCT_0:2;
reconsider D = addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! (H1(F),(0. F))),e #) as strict AbGroup by A1, Def4;
reconsider a = a, b = b as Element of D ;
reconsider x = a, y = b as Element of F ;
 (omf F) || (H1(F) \ {(0. F)}) is Function of [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):],(H1(F) \ {(0. F)}) by REALSET1:7;
then A2: dom ((omf F) || (H1(F) \ {(0. F)})) = [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] by FUNCT_2:def_1;
A3: for x, y being Element of H1(F) \ {(0. F)} holds (omf F) . (x,y) = the addF of D . (x,y)
proof
let x, y be Element of H1(F) \ {(0. F)}; ::_thesis: (omf F) . (x,y) = the addF of D . (x,y)
 [x,y] in [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] ;
hence  (omf F) . (x,y) = the addF of D . (x,y) by A2, FUNCT_1:47; ::_thesis: verum
end;
then x * y = a + b
.= b + a
.= y * x by A3 ;
hence  a * b = b * a ; ::_thesis: verum
end;

theorem Th6: :: REALSET2:6
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a being Element of NonZero F holds
( a * (1. F) = a & (1. F) * a = a )
proof
let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; ::_thesis: for a being Element of NonZero F holds
( a * (1. F) = a & (1. F) * a = a )
let a be Element of NonZero F; ::_thesis: ( a * (1. F) = a & (1. F) * a = a )
set B = H1(F) \ {(0. F)};
set P = (omf F) ! (H1(F),(0. F));
A1: H1(F) \ {(0. F)} = NonZero F ;
then reconsider e = 1. F as Element of H1(F) \ {(0. F)} by STRUCT_0:2;
reconsider D = addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! (H1(F),(0. F))),e #) as strict AbGroup by A1, Def4;
reconsider a = a as Element of D ;
 (omf F) || (H1(F) \ {(0. F)}) is Function of [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):],(H1(F) \ {(0. F)}) by REALSET1:7;
then A2: dom ((omf F) || (H1(F) \ {(0. F)})) = [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] by FUNCT_2:def_1;
A3: for x, y being Element of H1(F) \ {(0. F)} holds (omf F) . (x,y) = the addF of D . (x,y)
proof
let x, y be Element of H1(F) \ {(0. F)}; ::_thesis: (omf F) . (x,y) = the addF of D . (x,y)
 [x,y] in [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] ;
hence  (omf F) . (x,y) = the addF of D . (x,y) by A2, FUNCT_1:47; ::_thesis: verum
end;
then A4: (omf F) . ((1. F),a) = (0. D) + a
.= a by RLVECT_1:def_13 ;
(omf F) . (a,(1. F)) = a + (0. D) by A3
.= a by RLVECT_1:def_4 ;
hence  ( a * (1. F) = a & (1. F) * a = a ) by A4; ::_thesis: verum
end;

theorem Th7: :: REALSET2:7
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a being Element of NonZero F ex b being Element of NonZero F st
( a * b = 1. F & b * a = 1. F )
proof
let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; ::_thesis: for a being Element of NonZero F ex b being Element of NonZero F st
( a * b = 1. F & b * a = 1. F )
let a be Element of NonZero F; ::_thesis: ex b being Element of NonZero F st
( a * b = 1. F & b * a = 1. F )
set B = H1(F) \ {(0. F)};
set P = (omf F) ! (H1(F),(0. F));
A1: H1(F) \ {(0. F)} = NonZero F ;
then reconsider e = 1. F as Element of H1(F) \ {(0. F)} by STRUCT_0:2;
 addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! (H1(F),(0. F))),e #) is AbGroup by A1, Def4;
then consider D being strict AbGroup such that
A2: D = addLoopStr(# (H1(F) \ {(0. F)}),((omf F) ! (H1(F),(0. F))),e #) ;
reconsider a = a as Element of D by A2;
consider b being Element of D such that
A3: a + b = 0. D and
A4: b + a = 0. D by Th3;
reconsider b = b as Element of NonZero F by A2;
take  b ; ::_thesis: ( a * b = 1. F & b * a = 1. F )
 (omf F) || (H1(F) \ {(0. F)}) is Function of [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):],(H1(F) \ {(0. F)}) by REALSET1:7;
then A5: dom ((omf F) || (H1(F) \ {(0. F)})) = [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] by FUNCT_2:def_1;
 for x, y being Element of H1(F) \ {(0. F)} holds (omf F) . (x,y) = the addF of D . (x,y)
proof
let x, y be Element of H1(F) \ {(0. F)}; ::_thesis: (omf F) . (x,y) = the addF of D . (x,y)
 [x,y] in [:(H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}):] ;
hence  (omf F) . (x,y) = the addF of D . (x,y) by A2, A5, FUNCT_1:47; ::_thesis: verum
end;
hence  ( a * b = 1. F & b * a = 1. F ) by A2, A3, A4; ::_thesis: verum
end;

theorem :: REALSET2:8
for F being Field
for x, y being Element of F st x + y = 0. F holds
y = (comp F) . x
proof
let F be Field; ::_thesis: for x, y being Element of F st x + y = 0. F holds
y = (comp F) . x
let x, y be Element of F; ::_thesis: ( x + y = 0. F implies y = (comp F) . x )
assume  x + y = 0. F ; ::_thesis: y = (comp F) . x
then  y = - x by RLVECT_1:6;
hence  y = (comp F) . x by VECTSP_1:def_13; ::_thesis: verum
end;

theorem :: REALSET2:9
for F being Field
for x being Element of F holds x = (comp F) . ((comp F) . x)
proof
let F be Field; ::_thesis: for x being Element of F holds x = (comp F) . ((comp F) . x)
let x be Element of F; ::_thesis: x = (comp F) . ((comp F) . x)
thus x = - (- x) by RLVECT_1:17
.= (comp F) . (- x) by VECTSP_1:def_13
.= (comp F) . ((comp F) . x) by VECTSP_1:def_13 ; ::_thesis: verum
end;

theorem :: REALSET2:10
for F being Field
for a, b being Element of the carrier of F holds
( the addF of F . (a,b) is Element of the carrier of F & (omf F) . (a,b) is Element of the carrier of F & (comp F) . a is Element of the carrier of F ) ;

theorem :: REALSET2:11
for F being Field
for a, b, c being Element of F holds a * (b - c) = (a * b) - (a * c) by VECTSP_1:11;

theorem :: REALSET2:12
for F being Field
for a, b, c being Element of F holds (a - b) * c = (a * c) - (b * c) by VECTSP_1:13;

theorem :: REALSET2:13
for F being Field
for a being Element of F holds a * (0. F) = 0. F by VECTSP_1:6;

theorem :: REALSET2:14
for F being Field
for a being Element of F holds (0. F) * a = 0. F by VECTSP_1:7;

theorem :: REALSET2:15
for F being Field
for a, b being Element of F holds - (a * b) = a * (- b) by VECTSP_1:8;

theorem :: REALSET2:16
for F being Field holds (1. F) * (0. F) = 0. F by VECTSP_1:6;

theorem :: REALSET2:17
for F being Field holds (0. F) * (1. F) = 0. F by VECTSP_1:7;

theorem :: REALSET2:18
for F being Field
for a, b being Element of the carrier of F holds (omf F) . (a,b) is Element of the carrier of F ;

theorem Th19: :: REALSET2:19
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b, c being Element of F holds (a * b) * c = a * (b * c)
proof
let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; ::_thesis: for a, b, c being Element of F holds (a * b) * c = a * (b * c)
let a, b, c be Element of H1(F); ::_thesis: (a * b) * c = a * (b * c)
A1: ( a = 0. F implies (a * b) * c = a * (b * c) )
proof
assume A2: a = 0. F ; ::_thesis: (a * b) * c = a * (b * c)
hence (a * b) * c = (0. F) * c by VECTSP_1:7
.= 0. F by VECTSP_1:7
.= a * (b * c) by A2, VECTSP_1:7 ;
::_thesis: verum
end;
A3: ( b = 0. F implies (a * b) * c = a * (b * c) )
proof
assume A4: b = 0. F ; ::_thesis: (a * b) * c = a * (b * c)
hence (a * b) * c = (0. F) * c by VECTSP_1:6
.= 0. F by VECTSP_1:7
.= a * (0. F) by VECTSP_1:6
.= a * (b * c) by A4, VECTSP_1:7 ;
::_thesis: verum
end;
A5: ( c = 0. F implies (a * b) * c = a * (b * c) )
proof
assume A6: c = 0. F ; ::_thesis: (a * b) * c = a * (b * c)
hence (a * b) * c = 0. F by VECTSP_1:6
.= a * (0. F) by VECTSP_1:6
.= a * (b * c) by A6, VECTSP_1:6 ;
::_thesis: verum
end;
 ( a = 0. F or b = 0. F or c = 0. F or ( a is Element of NonZero F & b is Element of NonZero F & c is Element of NonZero F ) ) by ZFMISC_1:56;
hence  (a * b) * c = a * (b * c) by A1, A3, A5, Th4; ::_thesis: verum
end;

theorem Th20: :: REALSET2:20
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b being Element of F holds a * b = b * a
proof
let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; ::_thesis: for a, b being Element of F holds a * b = b * a
let a, b be Element of H1(F); ::_thesis: a * b = b * a
A1: ( a = 0. F implies a * b = b * a )
proof
assume A2: a = 0. F ; ::_thesis: a * b = b * a
then a * b = 0. F by VECTSP_1:7
.= b * a by A2, VECTSP_1:6 ;
hence  a * b = b * a ; ::_thesis: verum
end;
A3: ( b = 0. F implies a * b = b * a )
proof
assume A4: b = 0. F ; ::_thesis: a * b = b * a
then a * b = 0. F by VECTSP_1:6
.= b * a by A4, VECTSP_1:7 ;
hence  a * b = b * a ; ::_thesis: verum
end;
 ( a = 0. F or b = 0. F or ( a is Element of NonZero F & b is Element of NonZero F ) ) by ZFMISC_1:56;
hence  a * b = b * a by A1, A3, Th5; ::_thesis: verum
end;

theorem Th21: :: REALSET2:21
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a being Element of F holds
( a * (1. F) = a & (1. F) * a = a )
proof
let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; ::_thesis: for a being Element of F holds
( a * (1. F) = a & (1. F) * a = a )
let a be Element of H1(F); ::_thesis: ( a * (1. F) = a & (1. F) * a = a )
percases ( a = 0. F or a is Element of NonZero F ) by ZFMISC_1:56;
supposeA1: a = 0. F ; ::_thesis: ( a * (1. F) = a & (1. F) * a = a )
hence  a * (1. F) = a by VECTSP_1:7; ::_thesis: (1. F) * a = a
thus  (1. F) * a = a by A1, VECTSP_1:6; ::_thesis: verum
end;
suppose a is Element of NonZero F ; ::_thesis: ( a * (1. F) = a & (1. F) * a = a )
hence  ( a * (1. F) = a & (1. F) * a = a ) by Th6; ::_thesis: verum
end;
end;
end;

definition
let F be Field;
func revf F ->  UnOp of (NonZero F) means :Def6: :: REALSET2:def 6
 for x being Element of NonZero F holds (omf F) . (x,(it . x)) = 1. F;
existence
 ex b1 being UnOp of (NonZero F) st
for x being Element of NonZero F holds (omf F) . (x,(b1 . x)) = 1. F
proof
defpred S1[ set , set ] means (omf F) . ($1,$2) = 1. F;
A1: for x being set st x in H1(F) \ {(0. F)} holds
ex y being set st
( y in H1(F) \ {(0. F)} & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in H1(F) \ {(0. F)} implies ex y being set st
( y in H1(F) \ {(0. F)} & S1[x,y] ) )
assume  x in H1(F) \ {(0. F)} ; ::_thesis: ex y being set st
( y in H1(F) \ {(0. F)} & S1[x,y] )
then reconsider x = x as Element of NonZero F ;
consider y being Element of H1(F) \ {(0. F)} such that
A2: x * y = 1. F and
 y * x = 1. F by Th7;
reconsider y = y as set ;
take  y ; ::_thesis: ( y in H1(F) \ {(0. F)} & S1[x,y] )
thus  ( y in H1(F) \ {(0. F)} & S1[x,y] ) by A2; ::_thesis: verum
end;
 ex C being Function of (H1(F) \ {(0. F)}),(H1(F) \ {(0. F)}) st
for x being set st x in H1(F) \ {(0. F)} holds
S1[x,C . x] from FUNCT_2:sch_1(A1);
then consider C being UnOp of (NonZero F) such that
A3: for x being set st x in H1(F) \ {(0. F)} holds
(omf F) . (x,(C . x)) = 1. F ;
take  C ; ::_thesis: for x being Element of NonZero F holds (omf F) . (x,(C . x)) = 1. F
thus  for x being Element of NonZero F holds (omf F) . (x,(C . x)) = 1. F by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being UnOp of (NonZero F) st ( for x being Element of NonZero F holds (omf F) . (x,(b1 . x)) = 1. F ) & ( for x being Element of NonZero F holds (omf F) . (x,(b2 . x)) = 1. F ) holds
b1 = b2
proof
let C1, C2 be UnOp of (NonZero F); ::_thesis: ( ( for x being Element of NonZero F holds (omf F) . (x,(C1 . x)) = 1. F ) & ( for x being Element of NonZero F holds (omf F) . (x,(C2 . x)) = 1. F ) implies C1 = C2 )
assume that
A4: for x being Element of NonZero F holds (omf F) . (x,(C1 . x)) = 1. F and
A5: for x being Element of NonZero F holds (omf F) . (x,(C2 . x)) = 1. F ; ::_thesis: C1 = C2
 for x being set st x in H1(F) \ {(0. F)} holds
C1 . x = C2 . x
proof
let x be set ; ::_thesis: ( x in H1(F) \ {(0. F)} implies C1 . x = C2 . x )
assume A6: x in H1(F) \ {(0. F)} ; ::_thesis: C1 . x = C2 . x
then A7: C1 . x is Element of NonZero F by FUNCT_2:5;
then reconsider a = x, C1a = C1 . x as Element of F by A6;
A8: C2 . x is Element of NonZero F by A6, FUNCT_2:5;
then reconsider C2a = C2 . x as Element of F ;
C1 . x = C1a * (1. F) by A7, Th6
.= C1a * (a * C2a) by A5, A6
.= (a * C1a) * C2a by A6, A7, A8, Th4
.= (1. F) * C2a by A4, A6
.= C2 . x by A8, Th6 ;
hence  C1 . x = C2 . x ; ::_thesis: verum
end;
hence  C1 = C2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines revf REALSET2:def_6_:_
 for F being Field
for b2 being UnOp of (NonZero F) holds
( b2 = revf F iff for x being Element of NonZero F holds (omf F) . (x,(b2 . x)) = 1. F );

theorem :: REALSET2:22
for F being Field
for x, y being Element of NonZero F st x * y = 1. F holds
y = (revf F) . x
proof
let F be Field; ::_thesis: for x, y being Element of NonZero F st x * y = 1. F holds
y = (revf F) . x
let x, y be Element of NonZero F; ::_thesis: ( x * y = 1. F implies y = (revf F) . x )
assume A1: x * y = 1. F ; ::_thesis: y = (revf F) . x
reconsider rx = (revf F) . x as Element of F by XBOOLE_0:def_5;
y = y * (1. F) by Th6
.= (omf F) . (y,(1. F))
.= y * (x * rx) by Def6
.= (1. F) * rx by A1, Th4
.= (revf F) . x by Th6 ;
hence  y = (revf F) . x ; ::_thesis: verum
end;

theorem :: REALSET2:23
for F being Field
for x being Element of NonZero F holds x = (revf F) . ((revf F) . x)
proof
let F be Field; ::_thesis: for x being Element of NonZero F holds x = (revf F) . ((revf F) . x)
let x be Element of NonZero F; ::_thesis: x = (revf F) . ((revf F) . x)
reconsider rx = (revf F) . x as Element of F by XBOOLE_0:def_5;
reconsider rrx = (revf F) . ((revf F) . x) as Element of F by XBOOLE_0:def_5;
x = x * (1. F) by Th6
.= (omf F) . (x,(1. F))
.= x * (rx * rrx) by Def6
.= (x * rx) * rrx by Th4
.= (omf F) . ((1. F),((revf F) . ((revf F) . x))) by Def6
.= (1. F) * rrx
.= (revf F) . ((revf F) . x) by Th6 ;
hence  x = (revf F) . ((revf F) . x) ; ::_thesis: verum
end;

theorem :: REALSET2:24
for F being Field
for a, b being Element of NonZero F holds
( (omf F) . (a,b) is Element of NonZero F & (revf F) . a is Element of NonZero F )
proof
let F be Field; ::_thesis: for a, b being Element of NonZero F holds
( (omf F) . (a,b) is Element of NonZero F & (revf F) . a is Element of NonZero F )
let a, b be Element of NonZero F; ::_thesis: ( (omf F) . (a,b) is Element of NonZero F & (revf F) . a is Element of NonZero F )
 [a,b] in [:(NonZero F),(NonZero F):] ;
hence  ( (omf F) . (a,b) is Element of NonZero F & (revf F) . a is Element of NonZero F ) by REALSET1:def_6; ::_thesis: verum
end;

theorem :: REALSET2:25
for F being Field
for a, b, c being Element of F st a + b = a + c holds
b = c by RLVECT_1:8;

theorem :: REALSET2:26
for F being Field
for a being Element of NonZero F
for b, c being Element of the carrier of F st a * b = a * c holds
b = c
proof
let F be Field; ::_thesis: for a being Element of NonZero F
for b, c being Element of the carrier of F st a * b = a * c holds
b = c
let a be Element of NonZero F; ::_thesis: for b, c being Element of the carrier of F st a * b = a * c holds
b = c
let b, c be Element of H1(F); ::_thesis: ( a * b = a * c implies b = c )
reconsider x = a as Element of F ;
assume A1: a * b = a * c ; ::_thesis: b = c
reconsider ra = (revf F) . a as Element of F by XBOOLE_0:def_5;
b = (1. F) * b by Th21
.= (omf F) . ((1. F),b)
.= (x * ra) * b by Def6
.= ra * (x * c) by A1, Th19
.= (x * ra) * c by Th19
.= (omf F) . ((1. F),c) by Def6
.= (1. F) * c
.= c by Th21 ;
hence  b = c ; ::_thesis: verum
end;

registration
cluster non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like  ->  non degenerated almost_left_invertible associative commutative well-unital for doubleLoopStr ;
coherence
 for b1 being non degenerated doubleLoopStr st b1 is Field-like & b1 is Abelian & b1 is distributive & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable holds
( b1 is commutative & b1 is associative & b1 is well-unital & b1 is almost_left_invertible )
proof
let L be non degenerated doubleLoopStr ; ::_thesis: ( L is Field-like & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable implies ( L is commutative & L is associative & L is well-unital & L is almost_left_invertible ) )
assume A1: ( L is Field-like & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable ) ; ::_thesis: ( L is commutative & L is associative & L is well-unital & L is almost_left_invertible )
then  for x, y being Element of L holds x * y = y * x by Th20;
hence  L is commutative by GROUP_1:def_12; ::_thesis: ( L is associative & L is well-unital & L is almost_left_invertible )
 for x, y, z being Element of L holds (x * y) * z = x * (y * z) by A1, Th19;
hence  L is associative by GROUP_1:def_3; ::_thesis: ( L is well-unital & L is almost_left_invertible )
 for x being Element of L holds
( x * (1. L) = x & (1. L) * x = x ) by A1, Th21;
hence  L is well-unital by VECTSP_1:def_6; ::_thesis: L is almost_left_invertible
let x be Element of L; :: according to ALGSTR_0:def_39 ::_thesis: ( x = 0. L or x is left_invertible )
assume  x <> 0. L ; ::_thesis: x is left_invertible
then  not x in {(0. L)} by TARSKI:def_1;
then reconsider x = x as Element of NonZero L by XBOOLE_0:def_5;
consider y being Element of NonZero L such that
 x * y = 1. L and
A2: y * x = 1. L by A1, Th7;
take  y ; :: according to ALGSTR_0:def_27 ::_thesis: y * x = 1. L
thus  y * x = 1. L by A2; ::_thesis: verum
end;
end;