let R be Ring; :: thesis:
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:

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

per cases ;

suppose R is degenerated ; :: thesis:

hence R is almost_trivial ; :: thesis:

end;

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

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:

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

per cases by A7, CARD_1:50, TARSKI:def 2;

suppose f . a = 0 ; :: thesis:

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:

end;

suppose f . a = 1 ; :: thesis:

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:

end;

end;

end;

hence R is almost_trivial ; :: thesis:

end;

end;

end;

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

now :: thesis:

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

now :: thesis:

let o be object ; :: thesis:
assume o in {[(0. R),(0. (Z/ 2))],[(1. R),(1. (Z/ 2))]} ; :: thesis:

per cases by TARSKI:def 2;

suppose o = [(0. R),(0. (Z/ 2))] ; :: thesis:

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

end;

suppose o = [(1. R),(1. (Z/ 2))] ; :: thesis:

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

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:

let x, y1, y2 be object ; :: thesis:
assume A11: ( [x,y1] in f & [x,y2] in f ) ; :: thesis:

per cases = [(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:

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 = [(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:

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

end;

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

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

end;

end;

end;

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

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 = [(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:

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

end;

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

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

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:

let o be object ; :: thesis:
assume o in the carrier of R ; :: thesis:
then reconsider a = o as Element of R ;

per cases by A8;

suppose a = 0. R ; :: thesis:

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

end;

suppose a = 1. R ; :: thesis:

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

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:
[(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:

end;

A21: now :: thesis:

let a, b be Element of R; :: thesis:

per cases by A8;

suppose a = 0. R ; :: thesis:

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

end;

suppose A22: a = 1. R ; :: thesis:

per cases by A8;

suppose b = 0. R ; :: thesis:

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

end;

suppose A23: b = 1. R ; :: thesis:

now :: thesis:

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

per cases by A8;

suppose y = 0. R ; :: thesis:

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

end;

suppose y = 1. R ; :: thesis:

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

end;

end;

end;

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

end;

end;

end;

end;

end;

now :: thesis:

let a, b be Element of R; :: thesis:

per cases by A8;

suppose a = 0. R ; :: thesis:

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

end;

suppose a = 1. R ; :: thesis:

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

end;

end;

end;

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

now :: thesis:

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

per cases by A8;

suppose a = 0. R ; :: thesis:

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

end;

suppose a = 1. R ; :: thesis:

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

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:

let o be object ; :: thesis:
assume o in rng f ; :: thesis:
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 by A8;

suppose a = 0. R ; :: thesis:

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

end;

suppose a = 1. R ; :: thesis:

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

end;

end;

end;

now :: thesis:

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

per cases by A33, CARD_1:50, TARSKI:def 2;

suppose o = 0 ; :: thesis:

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:

end;

suppose o = 1 ; :: thesis:

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:

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:

end;

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