let A be non empty set ; :: thesis: for B being Finite_Subset of A
for L being 0_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
let B be Finite_Subset of A; :: thesis: for L being 0_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
let L be 0_Lattice; :: thesis: for f, g being Function of A, the carrier of L st f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
let f, g be Function of A, the carrier of L; :: thesis: ( f | B = g | B implies FinJoin (B,f) = FinJoin (B,g) )
set J = the L_join of L;
A1: Bottom L = the_unity_wrt the L_join of L by Th28;
assume A2: f | B = g | B ; :: thesis: FinJoin (B,f) = FinJoin (B,g)

now

per cases ( B = {} or B <> {} ) ;

suppose A3: B = {} ; :: thesis: FinJoin (B,f) = FinJoin (B,g)

hence FinJoin (B,f) = the L_join of L $$ (({}. A),f)
.= Bottom L by A1, SETWISEO:31
.= the L_join of L $$ (({}. A),g) by A1, SETWISEO:31
.= FinJoin (B,g) by A3 ;
:: thesis: verum

end;

suppose B <> {} ; :: thesis: FinJoin (B,f) = FinJoin (B,g)

hence FinJoin (B,f) = FinJoin (B,g) by A2, Th49; :: thesis: verum

end;

end;

end;

hence FinJoin (B,f) = FinJoin (B,g) ; :: thesis: verum