Th0:
for F1, F2 being Ring st F1 is Subring of F2 & F2 is Subring of F1 holds
F1 == F2
proof
let F1,
F2 be
Ring;
( F1 is Subring of F2 & F2 is Subring of F1 implies F1 == F2 )
assume AS1:
(
F1 is
Subring of
F2 &
F2 is
Subring of
F1 )
;
F1 == F2
then B:
(
1. F1 = 1. F2 &
0. F1 = 0. F2 )
by C0SP1:def 3;
D:
( the
carrier of
F1 c= the
carrier of
F2 & the
carrier of
F2 c= the
carrier of
F1 )
by AS1, C0SP1:def 3;
then E:
the
carrier of
F1 = the
carrier of
F2
by TARSKI:2;
C: the
addF of
F1 =
the
addF of
F2 || the
carrier of
F1
by AS1, C0SP1:def 3
.=
the
addF of
F2
by E
;
the
multF of
F1 =
the
multF of
F2 || the
carrier of
F1
by AS1, C0SP1:def 3
.=
the
multF of
F2
by E
;
then
doubleLoopStr(# the
carrier of
F1, the
addF of
F1, the
multF of
F1, the
OneF of
F1, the
ZeroF of
F1 #)
= doubleLoopStr(# the
carrier of
F2, the
addF of
F2, the
multF of
F2, the
OneF of
F2, the
ZeroF of
F2 #)
by B, C, D, TARSKI:2;
hence
F1 == F2
by FIELD_7:def 1;
verum
end;
hence
( R1 == R2 iff ( R1 is Subring of R2 & R2 is Subring of R1 ) )
by Th0; verum