let V, C be set ; :: thesis: for A, B being Element of Fin (PFuncs V,C)
for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )
let A, B be Element of Fin (PFuncs V,C); :: thesis: for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )
let a be set ; :: thesis: ( a in A ^ B implies ex b, c being set st
( b in A & c in B & a = b \/ c ) )
assume a in A ^ B ; :: thesis: ex b, c being set st
( b in A & c in B & a = b \/ c )
then ex s, t being Element of PFuncs V,C st
( a = s \/ t & s in A & t in B & s tolerates t ) ;
hence ex b, c being set st
( b in A & c in B & a = b \/ c ) ; :: thesis: verum