let R be Relation; :: thesis: ( R is well-ordering implies for a being object st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic )
assume A1: R is well-ordering ; :: thesis: for a being object st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic
let a be object ; :: thesis: ( a in field R implies not R,R |_2 (R -Seg a) are_isomorphic )
assume A2: a in field R ; :: thesis: not R,R |_2 (R -Seg a) are_isomorphic
set S = R |_2 (R -Seg a);
set F = canonical_isomorphism_of (R,(R |_2 (R -Seg a)));
assume R,R |_2 (R -Seg a) are_isomorphic ; :: thesis: contradiction
then A3: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is_isomorphism_of R,R |_2 (R -Seg a) by A1, Def9;
then A4: dom (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field R ;
A5: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is one-to-one by A3;
A6: now :: thesis: for b, c being object st [b,c] in R & b <> c holds
( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c )
let b, c be object ; :: thesis: ( [b,c] in R & b <> c implies ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c ) )
assume that
A7: [b,c] in R and
A8: b <> c ; :: thesis: ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c )
[((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R |_2 (R -Seg a) by A3, A7;
hence [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R by XBOOLE_0:def 4; :: thesis: (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c
( b in field R & c in field R ) by A7, RELAT_1:15;
hence (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c by A4, A5, A8; :: thesis: verum
end;
A9: rng (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field (R |_2 (R -Seg a)) by A3;
field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;
then (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a in R -Seg a by A2, A4, A9, FUNCT_1:def 3;
then A10: ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a),a] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a <> a ) by Th1;
rng (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) c= field R by A9, Th13;
then [a,((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a)] in R by A1, A2, A4, A6, Th35;
hence contradiction by A1, A10, Lm3; :: thesis: verum