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: ( the L_join of L is having_a_unity & Bottom L = the_unity_wrt the L_join of L ) by Th28, Th67;
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:40
.= the L_join of L $$ ({}. A),g by A1, SETWISEO:40
.= 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