let I be non empty set ; :: thesis: for a, b, c, d being set
for i, j being Element of I holds
( c in ((i -singleton a) (\/) (j -singleton d)) . b iff ( ( b = i & c = a ) or ( b = j & c = d ) ) )
let a, b, c, d be set ; :: thesis: for i, j being Element of I holds
( c in ((i -singleton a) (\/) (j -singleton d)) . b iff ( ( b = i & c = a ) or ( b = j & c = d ) ) )
let i, j be Element of I; :: thesis: ( c in ((i -singleton a) (\/) (j -singleton d)) . b iff ( ( b = i & c = a ) or ( b = j & c = d ) ) )
hereby :: thesis: ( ( ( b = i & c = a ) or ( b = j & c = d ) ) implies c in ((i -singleton a) (\/) (j -singleton d)) . b )
assume A1: c in ((i -singleton a) (\/) (j -singleton d)) . b ; :: thesis: ( ( not b = i or not c = a ) implies ( b = j & c = d ) )
assume A2: ( not b = i or not c = a ) ; :: thesis: ( b = j & c = d )
b in dom ((i -singleton a) (\/) (j -singleton d)) by A1, FUNCT_1:def 2;
then b in I by PARTFUN1:def 2;
then c in ((i -singleton a) . b) \/ ((j -singleton d) . b) by A1, PBOOLE:def 4;
then ( c in (i -singleton a) . b or c in (j -singleton d) . b ) by XBOOLE_0:def 3;
hence ( b = j & c = d ) by A2, Th3; :: thesis: verum
end;
assume A3: ( ( b = i & c = a ) or ( b = j & c = d ) ) ; :: thesis: c in ((i -singleton a) (\/) (j -singleton d)) . b
then ( c in (i -singleton a) . b or c in (j -singleton d) . b ) by Th3;
then c in ((i -singleton a) . b) \/ ((j -singleton d) . b) by XBOOLE_0:def 3;
hence c in ((i -singleton a) (\/) (j -singleton d)) . b by A3, PBOOLE:def 4; :: thesis: verum