let L be lower-bounded modular LATTICE; L has_a_representation_of_type<= 2
set A = the carrier of L;
set D = BasicDF L;
set S = the ExtensionSeq2 of the carrier of L, BasicDF L;
set FS = union { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } ;
A1:
( the ExtensionSeq2 of the carrier of L, BasicDF L . 0) `1 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum }
;
A2:
the ExtensionSeq2 of the carrier of L, BasicDF L . 0 = [ the carrier of L,(BasicDF L)]
by Def11;
the carrier of L c= union { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum }
by A1, A2, ZFMISC_1:74;
then reconsider FS = union { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } as non empty set ;
reconsider FD = union { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum } as distance_function of FS,L by Th32;
alpha FD is join-preserving
proof
set f =
alpha FD;
let a,
b be
Element of
L;
WAYBEL_0:def 35 alpha FD preserves_sup_of {a,b}
A3:
ex_sup_of (alpha FD) .: {a,b},
EqRelLATT FS
by YELLOW_0:17;
consider e2 being
Equivalence_Relation of
FS such that A4:
e2 = (alpha FD) . b
and A5:
for
x,
y being
Element of
FS holds
(
[x,y] in e2 iff
FD . (
x,
y)
<= b )
by LATTICE5:def 8;
consider e1 being
Equivalence_Relation of
FS such that A6:
e1 = (alpha FD) . a
and A7:
for
x,
y being
Element of
FS holds
(
[x,y] in e1 iff
FD . (
x,
y)
<= a )
by LATTICE5:def 8;
consider e3 being
Equivalence_Relation of
FS such that A8:
e3 = (alpha FD) . (a "\/" b)
and A9:
for
x,
y being
Element of
FS holds
(
[x,y] in e3 iff
FD . (
x,
y)
<= a "\/" b )
by LATTICE5:def 8;
A10:
field e2 = FS
by ORDERS_1:12;
now for x, y being object st [x,y] in e2 holds
[x,y] in e3let x,
y be
object ;
( [x,y] in e2 implies [x,y] in e3 )A11:
b <= b "\/" a
by YELLOW_0:22;
assume A12:
[x,y] in e2
;
[x,y] in e3then reconsider x9 =
x,
y9 =
y as
Element of
FS by A10, RELAT_1:15;
FD . (
x9,
y9)
<= b
by A5, A12;
then
FD . (
x9,
y9)
<= b "\/" a
by A11, ORDERS_2:3;
hence
[x,y] in e3
by A9;
verum end;
then A13:
e2 c= e3
;
A14:
field e3 = FS
by ORDERS_1:12;
for
u,
v being
object st
[u,v] in e3 holds
[u,v] in e1 "\/" e2
proof
let u,
v be
object ;
( [u,v] in e3 implies [u,v] in e1 "\/" e2 )
A15:
Seg 4
= { n where n is Nat : ( 1 <= n & n <= 4 ) }
by FINSEQ_1:def 1;
then A16:
3
in Seg 4
;
assume A17:
[u,v] in e3
;
[u,v] in e1 "\/" e2
then reconsider x =
u,
y =
v as
Element of
FS by A14, RELAT_1:15;
A18:
FD . (
x,
y)
<= a "\/" b
by A9, A17;
then consider z1,
z2 being
Element of
FS such that A19:
FD . (
x,
z1)
= a
and A20:
FD . (
z1,
z2)
= ((FD . (x,y)) "\/" a) "/\" b
and A21:
FD . (
z2,
y)
= a
by Th33;
A22:
u in FS
by A14, A17, RELAT_1:15;
defpred S1[
set ,
object ]
means ( ( $1
= 1 implies $2
= x ) & ( $1
= 2 implies $2
= z1 ) & ( $1
= 3 implies $2
= z2 ) & ( $1
= 4 implies $2
= y ) );
A23:
for
m being
Nat st
m in Seg 4 holds
ex
w being
object st
S1[
m,
w]
proof
let m be
Nat;
( m in Seg 4 implies ex w being object st S1[m,w] )
assume A24:
m in Seg 4
;
ex w being object st S1[m,w]
per cases
( m = 1 or m = 2 or m = 3 or m = 4 )
by A24, Lm3;
suppose A25:
m = 1
;
ex w being object st S1[m,w]take
x
;
S1[m,x]thus
S1[
m,
x]
by A25;
verum end; suppose A26:
m = 2
;
ex w being object st S1[m,w]take
z1
;
S1[m,z1]thus
S1[
m,
z1]
by A26;
verum end; suppose A27:
m = 3
;
ex w being object st S1[m,w]take
z2
;
S1[m,z2]thus
S1[
m,
z2]
by A27;
verum end; suppose A28:
m = 4
;
ex w being object st S1[m,w]take
y
;
S1[m,y]thus
S1[
m,
y]
by A28;
verum end; end;
end;
ex
p being
FinSequence st
(
dom p = Seg 4 & ( for
k being
Nat st
k in Seg 4 holds
S1[
k,
p . k] ) )
from FINSEQ_1:sch 1(A23);
then consider h being
FinSequence such that A29:
dom h = Seg 4
and A30:
for
m being
Nat st
m in Seg 4 holds
( (
m = 1 implies
h . m = x ) & (
m = 2 implies
h . m = z1 ) & (
m = 3 implies
h . m = z2 ) & (
m = 4 implies
h . m = y ) )
;
A31:
len h = 4
by A29, FINSEQ_1:def 3;
A32:
4
in Seg 4
by A15;
A33:
1
in Seg 4
by A15;
then A34:
u = h . 1
by A30;
A35:
2
in Seg 4
by A15;
A36:
for
j being
Nat st 1
<= j &
j < len h holds
[(h . j),(h . (j + 1))] in e1 \/ e2
proof
let j be
Nat;
( 1 <= j & j < len h implies [(h . j),(h . (j + 1))] in e1 \/ e2 )
assume A37:
( 1
<= j &
j < len h )
;
[(h . j),(h . (j + 1))] in e1 \/ e2
per cases
( j = 1 or j = 2 or j = 3 )
by A31, A37, Lm4;
suppose A39:
j = 2
;
[(h . j),(h . (j + 1))] in e1 \/ e2
(FD . (x,y)) "\/" a <= (a "\/" b) "\/" a
by A18, WAYBEL_1:2;
then
(FD . (x,y)) "\/" a <= b "\/" (a "\/" a)
by LATTICE3:14;
then
(FD . (x,y)) "\/" a <= b "\/" a
by YELLOW_5:1;
then
((FD . (x,y)) "\/" a) "/\" b <= b "/\" (b "\/" a)
by WAYBEL_1:1;
then
((FD . (x,y)) "\/" a) "/\" b <= b
by LATTICE3:18;
then
[z1,z2] in e2
by A5, A20;
then
[(h . 2),z2] in e2
by A30, A35;
then
[(h . 2),(h . 3)] in e2
by A30, A16;
hence
[(h . j),(h . (j + 1))] in e1 \/ e2
by A39, XBOOLE_0:def 3;
verum end; end;
end;
v =
h . 4
by A30, A32
.=
h . (len h)
by A29, FINSEQ_1:def 3
;
hence
[u,v] in e1 "\/" e2
by A22, A31, A34, A36, EQREL_1:28;
verum
end;
then A41:
e3 c= e1 "\/" e2
;
A42:
field e1 = FS
by ORDERS_1:12;
now for x, y being object st [x,y] in e1 holds
[x,y] in e3let x,
y be
object ;
( [x,y] in e1 implies [x,y] in e3 )A43:
a <= a "\/" b
by YELLOW_0:22;
assume A44:
[x,y] in e1
;
[x,y] in e3then reconsider x9 =
x,
y9 =
y as
Element of
FS by A42, RELAT_1:15;
FD . (
x9,
y9)
<= a
by A7, A44;
then
FD . (
x9,
y9)
<= a "\/" b
by A43, ORDERS_2:3;
hence
[x,y] in e3
by A9;
verum end;
then
e1 c= e3
;
then
e1 \/ e2 c= e3
by A13, XBOOLE_1:8;
then A45:
e1 "\/" e2 c= e3
by EQREL_1:def 2;
dom (alpha FD) = the
carrier of
L
by FUNCT_2:def 1;
then sup ((alpha FD) .: {a,b}) =
sup {((alpha FD) . a),((alpha FD) . b)}
by FUNCT_1:60
.=
((alpha FD) . a) "\/" ((alpha FD) . b)
by YELLOW_0:41
.=
e1 "\/" e2
by A6, A4, LATTICE5:10
.=
(alpha FD) . (a "\/" b)
by A8, A45, A41
.=
(alpha FD) . (sup {a,b})
by YELLOW_0:41
;
hence
alpha FD preserves_sup_of {a,b}
by A3;
verum
end;
then reconsider f = alpha FD as Homomorphism of L,(EqRelLATT FS) by LATTICE5:14;
A46:
dom f = the carrier of L
by FUNCT_2:def 1;
A47:
ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS )
proof
A48:
{ the carrier of L} <> {{ the carrier of L}}
consider A9 being non
empty set ,
d9 being
distance_function of
A9,
L,
Aq9 being non
empty set ,
dq9 being
distance_function of
Aq9,
L such that A49:
Aq9,
dq9 is_extension2_of A9,
d9
and A50:
the
ExtensionSeq2 of the
carrier of
L,
BasicDF L . 0 = [A9,d9]
and A51:
the
ExtensionSeq2 of the
carrier of
L,
BasicDF L . (0 + 1) = [Aq9,dq9]
by Def11;
(
A9 = the
carrier of
L &
d9 = BasicDF L )
by A2, A50, XTUPLE_0:1;
then consider q being
QuadrSeq of
BasicDF L such that A52:
Aq9 = NextSet2 (BasicDF L)
and A53:
dq9 = NextDelta2 q
by A49;
ConsecutiveSet2 ( the
carrier of
L,
{})
= the
carrier of
L
by Th14;
then reconsider Q =
Quadr2 (
q,
{}) as
Element of
[: the carrier of L, the carrier of L, the carrier of L, the carrier of L:] ;
A54:
( the ExtensionSeq2 of the carrier of L, BasicDF L . 1) `2 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum }
;
succ {} c= DistEsti (BasicDF L)
by Th1;
then
{} in DistEsti (BasicDF L)
by ORDINAL1:21;
then A55:
{} in dom q
by LATTICE5:25;
then
q . {} in rng q
by FUNCT_1:def 3;
then
q . {} in { [u,v,a9,b9] where u, v is Element of the carrier of L, a9, b9 is Element of L : (BasicDF L) . (u,v) <= a9 "\/" b9 }
by LATTICE5:def 13;
then consider u,
v being
Element of the
carrier of
L,
a,
b being
Element of
L such that A56:
q . {} = [u,v,a,b]
and
(BasicDF L) . (
u,
v)
<= a "\/" b
;
consider e being
Equivalence_Relation of
FS such that A57:
e = f . b
and A58:
for
x,
y being
Element of
FS holds
(
[x,y] in e iff
FD . (
x,
y)
<= b )
by LATTICE5:def 8;
Quadr2 (
q,
{})
= [u,v,a,b]
by A55, A56, Def6;
then A59:
b = Q `4_4
;
[Aq9,dq9] `2 = NextDelta2 q
by A53;
then A60:
NextDelta2 q c= FD
by A54, A51, ZFMISC_1:74;
A61:
{{ the carrier of L}} in {{ the carrier of L},{{ the carrier of L}}}
by TARSKI:def 2;
then A62:
{{ the carrier of L}} in the
carrier of
L \/ {{ the carrier of L},{{ the carrier of L}}}
by XBOOLE_0:def 3;
take
e
;
( e in the carrier of (Image f) & e <> id FS )
e in rng f
by A46, A57, FUNCT_1:def 3;
hence
e in the
carrier of
(Image f)
by YELLOW_0:def 15;
e <> id FS
A63:
( the ExtensionSeq2 of the carrier of L, BasicDF L . 1) `1 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum }
;
[Aq9,dq9] `1 = NextSet2 (BasicDF L)
by A52;
then A64:
NextSet2 (BasicDF L) c= FS
by A63, A51, ZFMISC_1:74;
new_set2 the
carrier of
L =
new_set2 (ConsecutiveSet2 ( the carrier of L,{}))
by Th14
.=
ConsecutiveSet2 ( the
carrier of
L,
(succ {}))
by Th15
;
then
new_set2 the
carrier of
L c= NextSet2 (BasicDF L)
by Th1, Th21;
then A65:
new_set2 the
carrier of
L c= FS
by A64;
A66:
{{ the carrier of L}} in new_set2 the
carrier of
L
by A61, XBOOLE_0:def 3;
A67:
{ the carrier of L} in {{ the carrier of L},{{ the carrier of L}}}
by TARSKI:def 2;
then
{ the carrier of L} in the
carrier of
L \/ {{ the carrier of L},{{ the carrier of L}}}
by XBOOLE_0:def 3;
then reconsider W =
{ the carrier of L},
V =
{{ the carrier of L}} as
Element of
FS by A65, A66;
A68:
(
ConsecutiveSet2 ( the
carrier of
L,
{})
= the
carrier of
L &
ConsecutiveDelta2 (
q,
{})
= BasicDF L )
by Th14, Th18;
ConsecutiveDelta2 (
q,
(succ {})) =
new_bi_fun2 (
(BiFun ((ConsecutiveDelta2 (q,{})),(ConsecutiveSet2 ( the carrier of L,{})),L)),
(Quadr2 (q,{})))
by Th19
.=
new_bi_fun2 (
(BasicDF L),
Q)
by A68, LATTICE5:def 15
;
then
new_bi_fun2 (
(BasicDF L),
Q)
c= NextDelta2 q
by Th1, Th24;
then A69:
new_bi_fun2 (
(BasicDF L),
Q)
c= FD
by A60;
(
dom (new_bi_fun2 ((BasicDF L),Q)) = [:(new_set2 the carrier of L),(new_set2 the carrier of L):] &
{ the carrier of L} in new_set2 the
carrier of
L )
by A67, FUNCT_2:def 1, XBOOLE_0:def 3;
then
[{ the carrier of L},{{ the carrier of L}}] in dom (new_bi_fun2 ((BasicDF L),Q))
by A62, ZFMISC_1:87;
then FD . (
W,
V) =
(new_bi_fun2 ((BasicDF L),Q)) . (
{ the carrier of L},
{{ the carrier of L}})
by A69, GRFUNC_1:2
.=
(((BasicDF L) . ((Q `1_4),(Q `2_4))) "\/" (Q `3_4)) "/\" (Q `4_4)
by Def4
;
then
FD . (
W,
V)
<= b
by A59, YELLOW_0:23;
then
[{ the carrier of L},{{ the carrier of L}}] in e
by A58;
hence
e <> id FS
by A48, RELAT_1:def 10;
verum
end;
BasicDF L is onto
by LATTICE5:40;
then A74:
rng (BasicDF L) = the carrier of L
by FUNCT_2:def 3;
for w being object st w in the carrier of L holds
ex z being object st
( z in [:FS,FS:] & w = FD . z )
proof
let w be
object ;
( w in the carrier of L implies ex z being object st
( z in [:FS,FS:] & w = FD . z ) )
A75:
( the ExtensionSeq2 of the carrier of L, BasicDF L . 0) `1 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum }
;
A76:
( the ExtensionSeq2 of the carrier of L, BasicDF L . 0) `2 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum }
;
A77:
the
ExtensionSeq2 of the
carrier of
L,
BasicDF L . 0 = [ the carrier of L,(BasicDF L)]
by Def11;
A78:
BasicDF L c= FD
by A76, A77, ZFMISC_1:74;
assume
w in the
carrier of
L
;
ex z being object st
( z in [:FS,FS:] & w = FD . z )
then consider z being
object such that A79:
z in [: the carrier of L, the carrier of L:]
and A80:
(BasicDF L) . z = w
by A74, FUNCT_2:11;
take
z
;
( z in [:FS,FS:] & w = FD . z )
the
carrier of
L c= FS
by A75, A77, ZFMISC_1:74;
then
[: the carrier of L, the carrier of L:] c= [:FS,FS:]
by ZFMISC_1:96;
hence
z in [:FS,FS:]
by A79;
w = FD . z
z in dom (BasicDF L)
by A79, FUNCT_2:def 1;
hence
w = FD . z
by A80, A78, GRFUNC_1:2;
verum
end;
then
rng FD = the carrier of L
by FUNCT_2:10;
then A81:
FD is onto
by FUNCT_2:def 3;
reconsider FS = FS as non trivial set by A70;
take
FS
; LATTICE8:def 2 ex f being Homomorphism of L,(EqRelLATT FS) st
( f is V17() & Image f is finitely_typed & ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) & type_of (Image f) <= 2 )
reconsider f = f as Homomorphism of L,(EqRelLATT FS) ;
take
f
; ( f is V17() & Image f is finitely_typed & ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) & type_of (Image f) <= 2 )
thus
f is V17()
by A81, LATTICE5:15; ( Image f is finitely_typed & ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) & type_of (Image f) <= 2 )
reconsider FD = FD as distance_function of FS,L ;
thus
Image f is finitely_typed
( ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) & type_of (Image f) <= 2 )proof
take
FS
;
LATTICE8:def 1 ( ( for e being object st e in the carrier of (Image f) holds
e is Equivalence_Relation of FS ) & ex o being Element of NAT st
for e1, e2 being Equivalence_Relation of FS
for x, y being object st e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = o & x,y are_joint_by F,e1,e2 ) )
thus
for
e being
object st
e in the
carrier of
(Image f) holds
e is
Equivalence_Relation of
FS
ex o being Element of NAT st
for e1, e2 being Equivalence_Relation of FS
for x, y being object st e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = o & x,y are_joint_by F,e1,e2 )
take
2
+ 2
;
for e1, e2 being Equivalence_Relation of FS
for x, y being object st e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = 2 + 2 & x,y are_joint_by F,e1,e2 )
thus
for
e1,
e2 being
Equivalence_Relation of
FS for
x,
y being
object st
e1 in the
carrier of
(Image f) &
e2 in the
carrier of
(Image f) &
[x,y] in e1 "\/" e2 holds
ex
F being non
empty FinSequence of
FS st
(
len F = 2
+ 2 &
x,
y are_joint_by F,
e1,
e2 )
by Th34;
verum
end;
thus
ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS )
type_of (Image f) <= 2proof
A84:
{ the carrier of L} <> {{ the carrier of L}}
consider A9 being non
empty set ,
d9 being
distance_function of
A9,
L,
Aq9 being non
empty set ,
dq9 being
distance_function of
Aq9,
L such that A85:
Aq9,
dq9 is_extension2_of A9,
d9
and A86:
the
ExtensionSeq2 of the
carrier of
L,
BasicDF L . 0 = [A9,d9]
and A87:
the
ExtensionSeq2 of the
carrier of
L,
BasicDF L . (0 + 1) = [Aq9,dq9]
by Def11;
(
A9 = the
carrier of
L &
d9 = BasicDF L )
by A2, A86, XTUPLE_0:1;
then consider q being
QuadrSeq of
BasicDF L such that A88:
Aq9 = NextSet2 (BasicDF L)
and A89:
dq9 = NextDelta2 q
by A85;
ConsecutiveSet2 ( the
carrier of
L,
{})
= the
carrier of
L
by Th14;
then reconsider Q =
Quadr2 (
q,
{}) as
Element of
[: the carrier of L, the carrier of L, the carrier of L, the carrier of L:] ;
A90:
( the ExtensionSeq2 of the carrier of L, BasicDF L . 1) `2 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum }
;
succ {} c= DistEsti (BasicDF L)
by Th1;
then
{} in DistEsti (BasicDF L)
by ORDINAL1:21;
then A91:
{} in dom q
by LATTICE5:25;
then
q . {} in rng q
by FUNCT_1:def 3;
then
q . {} in { [u,v,a9,b9] where u, v is Element of the carrier of L, a9, b9 is Element of L : (BasicDF L) . (u,v) <= a9 "\/" b9 }
by LATTICE5:def 13;
then consider u,
v being
Element of the
carrier of
L,
a,
b being
Element of
L such that A92:
q . {} = [u,v,a,b]
and
(BasicDF L) . (
u,
v)
<= a "\/" b
;
consider e being
Equivalence_Relation of
FS such that A93:
e = f . b
and A94:
for
x,
y being
Element of
FS holds
(
[x,y] in e iff
FD . (
x,
y)
<= b )
by LATTICE5:def 8;
Quadr2 (
q,
{})
= [u,v,a,b]
by A91, A92, Def6;
then A95:
b = Q `4_4
;
[Aq9,dq9] `2 = NextDelta2 q
by A89;
then A96:
NextDelta2 q c= FD
by A90, A87, ZFMISC_1:74;
A97:
{{ the carrier of L}} in {{ the carrier of L},{{ the carrier of L}}}
by TARSKI:def 2;
then A98:
{{ the carrier of L}} in the
carrier of
L \/ {{ the carrier of L},{{ the carrier of L}}}
by XBOOLE_0:def 3;
take
e
;
( e in the carrier of (Image f) & e <> id FS )
e in rng f
by A46, A93, FUNCT_1:def 3;
hence
e in the
carrier of
(Image f)
by YELLOW_0:def 15;
e <> id FS
A99:
( the ExtensionSeq2 of the carrier of L, BasicDF L . 1) `1 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum }
;
[Aq9,dq9] `1 = NextSet2 (BasicDF L)
by A88;
then A100:
NextSet2 (BasicDF L) c= FS
by A99, A87, ZFMISC_1:74;
new_set2 the
carrier of
L =
new_set2 (ConsecutiveSet2 ( the carrier of L,{}))
by Th14
.=
ConsecutiveSet2 ( the
carrier of
L,
(succ {}))
by Th15
;
then
new_set2 the
carrier of
L c= NextSet2 (BasicDF L)
by Th1, Th21;
then A101:
new_set2 the
carrier of
L c= FS
by A100;
A102:
{{ the carrier of L}} in new_set2 the
carrier of
L
by A97, XBOOLE_0:def 3;
A103:
{ the carrier of L} in {{ the carrier of L},{{ the carrier of L}}}
by TARSKI:def 2;
then
{ the carrier of L} in the
carrier of
L \/ {{ the carrier of L},{{ the carrier of L}}}
by XBOOLE_0:def 3;
then reconsider W =
{ the carrier of L},
V =
{{ the carrier of L}} as
Element of
FS by A101, A102;
A104:
(
ConsecutiveSet2 ( the
carrier of
L,
{})
= the
carrier of
L &
ConsecutiveDelta2 (
q,
{})
= BasicDF L )
by Th14, Th18;
ConsecutiveDelta2 (
q,
(succ {})) =
new_bi_fun2 (
(BiFun ((ConsecutiveDelta2 (q,{})),(ConsecutiveSet2 ( the carrier of L,{})),L)),
(Quadr2 (q,{})))
by Th19
.=
new_bi_fun2 (
(BasicDF L),
Q)
by A104, LATTICE5:def 15
;
then
new_bi_fun2 (
(BasicDF L),
Q)
c= NextDelta2 q
by Th1, Th24;
then A105:
new_bi_fun2 (
(BasicDF L),
Q)
c= FD
by A96;
(
dom (new_bi_fun2 ((BasicDF L),Q)) = [:(new_set2 the carrier of L),(new_set2 the carrier of L):] &
{ the carrier of L} in new_set2 the
carrier of
L )
by A103, FUNCT_2:def 1, XBOOLE_0:def 3;
then
[{ the carrier of L},{{ the carrier of L}}] in dom (new_bi_fun2 ((BasicDF L),Q))
by A98, ZFMISC_1:87;
then FD . (
W,
V) =
(new_bi_fun2 ((BasicDF L),Q)) . (
{ the carrier of L},
{{ the carrier of L}})
by A105, GRFUNC_1:2
.=
(((BasicDF L) . ((Q `1_4),(Q `2_4))) "\/" (Q `3_4)) "/\" (Q `4_4)
by Def4
;
then
FD . (
W,
V)
<= b
by A95, YELLOW_0:23;
then
[{ the carrier of L},{{ the carrier of L}}] in e
by A94;
hence
e <> id FS
by A84, RELAT_1:def 10;
verum
end;
for e1, e2 being Equivalence_Relation of FS
for x, y being object st e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = 2 + 2 & x,y are_joint_by F,e1,e2 )
by Th34;
hence
type_of (Image f) <= 2
by A47, LATTICE5:13; verum