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, Th12;
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:91, ZFMISC_1:119;
A5:
SubstitutionSet V,C c= SubstitutionSet V9,C9
by A3, Th12;
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
set ;
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
set 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 5;
consider y1,
y2 being
set 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:72
.=
mi (y19 \/ y29)
by SUBSTLAT:def 4
.=
mi (y11 \/ y22)
by A3, Th13
;
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:4;
now let a,
b be
Element of
(SubstLatt V,C);
B1 . a,b = B2 . a,breconsider 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, Th13
.=
the
L_join of
(SubstLatt V9,C9) . a,
b
by SUBSTLAT:def 4
.=
B2 . [a,b]
by FUNCT_1:72
.=
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