let V, V9, C, C9 be set ; :: thesis: ( 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 ) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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))) ; :: thesis: 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; :: thesis: 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 :: thesis: 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)); :: thesis: 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) ; :: thesis: 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; :: thesis: verum