let V, V9, C, C9 be set ; ( V c= V9 & C c= C9 implies the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C)) )
set K = SubstLatt (V,C);
set L = SubstLatt (V9,C9);
A1:
SubstitutionSet (V,C) = the carrier of (SubstLatt (V,C))
by SUBSTLAT:def 4;
A2:
dom the L_join of (SubstLatt (V9,C9)) = [: the carrier of (SubstLatt (V9,C9)), the carrier of (SubstLatt (V9,C9)):]
by FUNCT_2:def 1;
reconsider B1 = the L_join of (SubstLatt (V,C)) as BinOp of the carrier of (SubstLatt (V,C)) ;
set B2 = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C));
assume A3:
( V c= V9 & C c= C9 )
; the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))
SubstitutionSet (V9,C9) = the carrier of (SubstLatt (V9,C9))
by SUBSTLAT:def 4;
then
the carrier of (SubstLatt (V,C)) c= the carrier of (SubstLatt (V9,C9))
by A1, A3, Th9;
then A4:
dom ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) = [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):]
by A2, RELAT_1:62, ZFMISC_1:96;
A5:
SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)
by A3, Th9;
rng ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) c= the carrier of (SubstLatt (V,C))
proof
let x be
object ;
TARSKI:def 3 ( not x in rng ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) or x in the carrier of (SubstLatt (V,C)) )
assume
x in rng ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C)))
;
x in the carrier of (SubstLatt (V,C))
then consider y being
object such that A6:
y in dom ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C)))
and A7:
x = ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) . y
by FUNCT_1:def 3;
consider y1,
y2 being
object such that A8:
(
y1 in the
carrier of
(SubstLatt (V,C)) &
y2 in the
carrier of
(SubstLatt (V,C)) )
and A9:
y = [y1,y2]
by A4, A6, ZFMISC_1:def 2;
(
y1 in SubstitutionSet (
V,
C) &
y2 in SubstitutionSet (
V,
C) )
by A8, SUBSTLAT:def 4;
then reconsider y19 =
y1,
y29 =
y2 as
Element of
SubstitutionSet (
V9,
C9)
by A5;
reconsider y11 =
y1,
y22 =
y2 as
Element of
SubstitutionSet (
V,
C)
by A8, SUBSTLAT:def 4;
( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) . y =
the
L_join of
(SubstLatt (V9,C9)) . (
y1,
y2)
by A4, A6, A9, FUNCT_1:49
.=
mi (y19 \/ y29)
by SUBSTLAT:def 4
.=
mi (y11 \/ y22)
by A3, Th10
;
hence
x in the
carrier of
(SubstLatt (V,C))
by A1, A7;
verum
end;
then reconsider B2 = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C)) as BinOp of the carrier of (SubstLatt (V,C)) by A4, FUNCT_2:2;
now for a, b being Element of (SubstLatt (V,C)) holds B1 . (a,b) = B2 . (a,b)let a,
b be
Element of
(SubstLatt (V,C));
B1 . (a,b) = B2 . (a,b)reconsider a9 =
a,
b9 =
b as
Element of
SubstitutionSet (
V,
C)
by SUBSTLAT:def 4;
(
a9 in SubstitutionSet (
V,
C) &
b9 in SubstitutionSet (
V,
C) )
;
then reconsider a1 =
a,
b1 =
b as
Element of
SubstitutionSet (
V9,
C9)
by A5;
thus B1 . (
a,
b) =
mi (a9 \/ b9)
by SUBSTLAT:def 4
.=
mi (a1 \/ b1)
by A3, Th10
.=
the
L_join of
(SubstLatt (V9,C9)) . (
a,
b)
by SUBSTLAT:def 4
.=
B2 . [a,b]
by FUNCT_1:49
.=
B2 . (
a,
b)
;
verum end;
hence
the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))
by BINOP_1:2; verum