let R be Ring; :: thesis: ( R is almost_trivial iff ( R is degenerated or R, Z/ 2 are_isomorphic ) )
A1: Z/ 2 = doubleLoopStr(# (Segm 2),(addint 2),(multint 2),(In (1,(Segm 2))),(In (0,(Segm 2))) #) by INT_3:def 12;

A2: now :: thesis: ( ( R is degenerated or R, Z/ 2 are_isomorphic ) implies R is almost_trivial )

assume ( R is degenerated or R, Z/ 2 are_isomorphic ) ; :: thesis: R is almost_trivial

per cases then ( R is degenerated or R, Z/ 2 are_isomorphic ) ;

suppose R is degenerated ; :: thesis: R is almost_trivial

hence R is almost_trivial ; :: thesis: verum

end;

suppose R, Z/ 2 are_isomorphic ; :: thesis: R is almost_trivial

then consider f being Function of R,(Z/ 2) such that
A4: f is isomorphism by QUOFIELD:def 23;
( f is monomorphism & f is onto ) by A4, MOD_4:def 12;
then A5: ( f is linear & f is one-to-one ) by MOD_4:def 8;

now :: thesis: for a being Element of R holds
( a = 1. R or a = 0. R )

let a be Element of R; :: thesis: ( b₁ = 1. R or b₁ = 0. R )
A6: dom f = [#] R by FUNCT_2:def 1;
A7: [#] (INT.Ring 2) = 2 by A1, ORDINAL1:def 17;

per cases ( f . a = 0 or f . a = 1 ) by A7, CARD_1:50, TARSKI:def 2;

suppose f . a = 0 ; :: thesis: ( b₁ = 1. R or b₁ = 0. R )

then f . a = 0. (Z/ 2) by A1
.= f . (0. R) by A5, RING_2:6 ;
hence ( a = 1. R or a = 0. R ) by A5, A6; :: thesis: verum

end;

suppose f . a = 1 ; :: thesis: ( b₁ = 1. R or b₁ = 0. R )

then f . a = 1_ (Z/ 2) by INT_3:14
.= f . (1_ R) by A5, GROUP_1:def 13
.= f . (1. R) ;
hence ( a = 1. R or a = 0. R ) by A5, A6; :: thesis: verum

end;

end;

end;

hence R is almost_trivial ; :: thesis: verum

end;

end;

end;

set A = the carrier of R;
set B = the carrier of (Z/ 2);

now :: thesis: ( R is almost_trivial & not R is degenerated implies R, Z/ 2 are_isomorphic )

assume that
A8: R is almost_trivial and
A9: not R is degenerated ; :: thesis: R, Z/ 2 are_isomorphic
set f = {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]};

now :: thesis: for o being object st o in {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} holds
o in [: the carrier of R, the carrier of (Z/ 2):]

let o be object ; :: thesis: ( o in {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} implies b₁ in [: the carrier of R, the carrier of (Z/ 2):] )
assume o in {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} ; :: thesis: b₁ in [: the carrier of R, the carrier of (Z/ 2):]

per cases then ( o = [(0. R),(0. (Z/ 2))] or o = [(1. R),(1. (Z/ 2))] ) by TARSKI:def 2;

suppose o = [(0. R),(0. (Z/ 2))] ; :: thesis: b₁ in [: the carrier of R, the carrier of (Z/ 2):]

hence o in [: the carrier of R, the carrier of (Z/ 2):] by ZFMISC_1:def 2; :: thesis: verum

end;

suppose o = [(1. R),(1. (Z/ 2))] ; :: thesis: b₁ in [: the carrier of R, the carrier of (Z/ 2):]

hence o in [: the carrier of R, the carrier of (Z/ 2):] by ZFMISC_1:def 2; :: thesis: verum

end;

end;

end;

then reconsider f = {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} as Subset of [: the carrier of R, the carrier of (Z/ 2):] by TARSKI:def 3;
reconsider f = f as Relation of the carrier of R, the carrier of (Z/ 2) ;

now :: thesis: for x, y1, y2 being object st [x,y1] in f & [x,y2] in f holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in f & [x,y2] in f implies b₂ = b₃ )
assume A11: ( [x,y1] in f & [x,y2] in f ) ; :: thesis: b₂ = b₃

per cases then ( [x,y1] = [(0. R),(0. (Z/ 2))] or [x,y1] = [(1. R),(1. (Z/ 2))] ) by TARSKI:def 2;

suppose A12: [x,y1] = [(0. R),(0. (Z/ 2))] ; :: thesis: b₂ = b₃

A13: y1 = [(0. R),(0. (Z/ 2))] `2 by A12
.= 0. (Z/ 2) ;
A14: x = [(0. R),(0. (Z/ 2))] `1 by A12
.= 0. R ;

per cases ( [x,y2] = [(0. R),(0. (Z/ 2))] or [x,y2] = [(1. R),(1. (Z/ 2))] ) by A11, TARSKI:def 2;

suppose [x,y2] = [(0. R),(0. (Z/ 2))] ; :: thesis: b₂ = b₃

then y2 = [(0. R),(0. (Z/ 2))] `2
.= 0. (Z/ 2) ;
hence y1 = y2 by A13; :: thesis: verum

end;

suppose [x,y2] = [(1. R),(1. (Z/ 2))] ; :: thesis: b₂ = b₃

then x = [(1. R),(1. (Z/ 2))] `1
.= 1. R ;
hence y1 = y2 by A14, A9; :: thesis: verum

end;

end;

end;

suppose A15: [x,y1] = [(1. R),(1. (Z/ 2))] ; :: thesis: b₂ = b₃

then A16: y1 = [(1. R),(1. (Z/ 2))] `2
.= 1. (Z/ 2) ;
A17: x = [(1. R),(1. (Z/ 2))] `1 by A15
.= 1. R ;

per cases ( [x,y2] = [(0. R),(0. (Z/ 2))] or [x,y2] = [(1. R),(1. (Z/ 2))] ) by A11, TARSKI:def 2;

suppose [x,y2] = [(0. R),(0. (Z/ 2))] ; :: thesis: b₂ = b₃

then x = [(0. R),(0. (Z/ 2))] `1
.= 0. R ;
hence y1 = y2 by A17, A9; :: thesis: verum

end;

suppose [x,y2] = [(1. R),(1. (Z/ 2))] ; :: thesis: b₂ = b₃

then y2 = [(1. R),(1. (Z/ 2))] `2
.= 1. (Z/ 2) ;
hence y1 = y2 by A16; :: thesis: verum

end;

end;

end;

end;

end;

then reconsider f = f as PartFunc of the carrier of R, the carrier of (Z/ 2) by FUNCT_1:def 1;
A18: dom f c= the carrier of R ;

now :: thesis: for o being object st o in the carrier of R holds
o in dom f

let o be object ; :: thesis: ( o in the carrier of R implies b₁ in dom f )
assume o in the carrier of R ; :: thesis: b₁ in dom f
then reconsider a = o as Element of R ;

per cases ( a = 0. R or a = 1. R ) by A8;

suppose a = 0. R ; :: thesis: b₁ in dom f

then [a,(0. (Z/ 2))] in f by TARSKI:def 2;
hence o in dom f by FUNCT_1:1; :: thesis: verum

end;

suppose a = 1. R ; :: thesis: b₁ in dom f

then [a,(1. (Z/ 2))] in f by TARSKI:def 2;
hence o in dom f by FUNCT_1:1; :: thesis: verum

end;

end;

end;

then A19: dom f = the carrier of R by A18, TARSKI:2;
reconsider f = f as Function of the carrier of R, the carrier of (Z/ 2) by A19, FUNCT_2:def 1;
A20: ( f . (0. R) = 0. (Z/ 2) & f . (1. R) = 1. (Z/ 2) )

proof

[(0. R),(0. (Z/ 2))] in f by TARSKI:def 2;
hence f . (0. R) = 0. (Z/ 2) by A19, FUNCT_1:def 2; :: thesis: f . (1. R) = 1. (Z/ 2)
[(1. R),(1. (Z/ 2))] in f by TARSKI:def 2;
hence f . (1. R) = 1. (Z/ 2) by A19, FUNCT_1:def 2; :: thesis: verum

end;

A21: now :: thesis: for a, b being Element of R holds f . (a + b) = (f . a) + (f . b)

let a, b be Element of R; :: thesis: f . (b₁ + b₂) = (f . b₁) + (f . b₂)

per cases ( a = 0. R or a = 1. R ) by A8;

suppose a = 0. R ; :: thesis: f . (b₁ + b₂) = (f . b₁) + (f . b₂)

hence f . (a + b) = (f . a) + (f . b) by A20; :: thesis: verum

end;

suppose A22: a = 1. R ; :: thesis: f . (b₁ + b₂) = (f . b₁) + (f . b₂)

per cases ( b = 0. R or b = 1. R ) by A8;

suppose b = 0. R ; :: thesis: f . (b₁ + b₂) = (f . b₁) + (f . b₂)

hence f . (a + b) = (f . a) + (f . b) by A20; :: thesis: verum

end;

suppose A23: b = 1. R ; :: thesis: f . (b₁ + b₂) = (f . b₁) + (f . b₂)

now :: thesis: not a + b = 1. R

assume A24: a + b = 1. R ; :: thesis: contradiction
consider y being Element of R such that
A25: a + y = 0. R by ALGSTR_0:def 11;

per cases ( y = 0. R or y = 1. R ) by A8;

suppose y = 0. R ; :: thesis: contradiction

hence contradiction by A20, A22, A25; :: thesis: verum

end;

suppose y = 1. R ; :: thesis: contradiction

hence contradiction by A24, A25, A23, A20; :: thesis: verum

end;

end;

end;

hence f . (a + b) = (f . a) + (f . b) by A8, A20, Th5, A23, A22; :: thesis: verum

end;

end;

end;

end;

end;

now :: thesis: for a, b being Element of R holds f . (a * b) = (f . a) * (f . b)

let a, b be Element of R; :: thesis: f . (b₁ * b₂) = (f . b₁) * (f . b₂)

per cases ( a = 0. R or a = 1. R ) by A8;

suppose a = 0. R ; :: thesis: f . (b₁ * b₂) = (f . b₁) * (f . b₂)

hence f . (a * b) = (f . a) * (f . b) by A20; :: thesis: verum

end;

suppose a = 1. R ; :: thesis: f . (b₁ * b₂) = (f . b₁) * (f . b₂)

hence f . (a * b) = (f . a) * (f . b) by A20; :: thesis: verum

end;

end;

end;

then A28: ( f is additive & f is multiplicative & f is unity-preserving ) by A20, A21, GROUP_6:def 6;

now :: thesis: for x, y being object st x in the carrier of R & y in the carrier of R & f . x = f . y holds
x = y

let x, y be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & f . x = f . y implies b₁ = b₂ )
assume A29: ( x in the carrier of R & y in the carrier of R & f . x = f . y ) ; :: thesis: b₁ = b₂
then reconsider a = x, b = y as Element of R ;

per cases ( a = 0. R or a = 1. R ) by A8;

suppose a = 0. R ; :: thesis: b₁ = b₂

hence x = y by A8, A20, A29; :: thesis: verum

end;

suppose a = 1. R ; :: thesis: b₁ = b₂

hence x = y by A8, A20, A29; :: thesis: verum

end;

end;

end;

then f is one-to-one by FUNCT_2:19;
then A30: f is monomorphism by A28, MOD_4:def 8;

A31: now :: thesis: for o being object st o in rng f holds
o in the carrier of (Z/ 2)

let o be object ; :: thesis: ( o in rng f implies b₁ in the carrier of (Z/ 2) )
assume o in rng f ; :: thesis: b₁ in the carrier of (Z/ 2)
then consider x being object such that
A32: ( x in dom f & o = f . x ) by FUNCT_1:def 3;
reconsider a = x as Element of R by A32;

per cases ( a = 0. R or a = 1. R ) by A8;

suppose a = 0. R ; :: thesis: b₁ in the carrier of (Z/ 2)

hence o in the carrier of (Z/ 2) by A20, A32; :: thesis: verum

end;

suppose a = 1. R ; :: thesis: b₁ in the carrier of (Z/ 2)

hence o in the carrier of (Z/ 2) by A20, A32; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in the carrier of (Z/ 2) holds
o in rng f

let o be object ; :: thesis: ( o in the carrier of (Z/ 2) implies b₁ in rng f )
assume o in the carrier of (Z/ 2) ; :: thesis: b₁ in rng f
then A33: o in 2 by A1, ORDINAL1:def 17;

per cases ( o = 0 or o = 1 ) by A33, CARD_1:50, TARSKI:def 2;

suppose o = 0 ; :: thesis: b₁ in rng f

then o = f . (0. R) by A1, A20, NAT_1:44, SUBSET_1:def 8;
hence o in rng f by A19, FUNCT_1:def 3; :: thesis: verum

end;

suppose o = 1 ; :: thesis: b₁ in rng f

then o = f . (1. R) by A20, A1, NAT_1:44, SUBSET_1:def 8;
hence o in rng f by A19, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

then f is onto by A31, TARSKI:2;
hence R, Z/ 2 are_isomorphic by A30, MOD_4:def 12, QUOFIELD:def 23; :: thesis: verum

end;

hence ( R is almost_trivial iff ( R is degenerated or R, Z/ 2 are_isomorphic ) ) by A2; :: thesis: verum