let V, V', C, C' be set ; ( V c= V' & C c= C' implies the L_join of (SubstLatt V,C) = the L_join of (SubstLatt V',C') || the carrier of (SubstLatt V,C) )
set K = SubstLatt V,C;
set L = SubstLatt V',C';
A1:
SubstitutionSet V,C = the carrier of (SubstLatt V,C)
by SUBSTLAT:def 4;
A2:
dom the L_join of (SubstLatt V',C') = [:the carrier of (SubstLatt V',C'),the carrier of (SubstLatt V',C'):]
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 V',C') || the carrier of (SubstLatt V,C);
assume A3:
( V c= V' & C c= C' )
; the L_join of (SubstLatt V,C) = the L_join of (SubstLatt V',C') || the carrier of (SubstLatt V,C)
SubstitutionSet V',C' = the carrier of (SubstLatt V',C')
by SUBSTLAT:def 4;
then
the carrier of (SubstLatt V,C) c= the carrier of (SubstLatt V',C')
by A1, A3, Th12;
then A4:
dom (the L_join of (SubstLatt V',C') || 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 V',C'
by A3, Th12;
rng (the L_join of (SubstLatt V',C') || 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 V',C') || the carrier of (SubstLatt V,C)) or x in the carrier of (SubstLatt V,C) )
assume
x in rng (the L_join of (SubstLatt V',C') || 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 V',C') || the carrier of (SubstLatt V,C))
and A7:
x = (the L_join of (SubstLatt V',C') || 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 y1' =
y1,
y2' =
y2 as
Element of
SubstitutionSet V',
C' by A5;
reconsider y11 =
y1,
y22 =
y2 as
Element of
SubstitutionSet V,
C by A8, SUBSTLAT:def 4;
(the L_join of (SubstLatt V',C') || the carrier of (SubstLatt V,C)) . y =
the
L_join of
(SubstLatt V',C') . y1,
y2
by A4, A6, A9, FUNCT_1:72
.=
mi (y1' \/ y2')
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 V',C') || 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 ;
B1 . a,b = B2 . a,breconsider a' =
a,
b' =
b as
Element of
SubstitutionSet V,
C by SUBSTLAT:def 4;
(
a' in SubstitutionSet V,
C &
b' in SubstitutionSet V,
C )
;
then reconsider a1 =
a,
b1 =
b as
Element of
SubstitutionSet V',
C' by A5;
thus B1 . a,
b =
mi (a' \/ b')
by SUBSTLAT:def 4
.=
mi (a1 \/ b1)
by A3, Th13
.=
the
L_join of
(SubstLatt V',C') . 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 V',C') || the carrier of (SubstLatt V,C)
by BINOP_1:2; verum