let X be set ; :: thesis: for B being disjoint_valued FinSequence of bool X
for a, b, c being object st a in B . b & a in B . c holds
( b = c & b in dom B )
let B be disjoint_valued FinSequence of bool X; :: thesis: for a, b, c being object st a in B . b & a in B . c holds
( b = c & b in dom B )
let a, b, c be object ; :: thesis: ( a in B . b & a in B . c implies ( b = c & b in dom B ) )
assume that
A1: a in B . b and
A2: a in B . c ; :: thesis: ( b = c & b in dom B )
A3: b in dom B by A1, FUNCT_1:def 2;
A4: c in dom B by A2, FUNCT_1:def 2;
B . b meets B . c by A1, A2, XBOOLE_0:def 4;
hence ( b = c & b in dom B ) by A3, A4, Def13; :: thesis: verum