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 c being set st
( c in B & c c= a )
let A, B be Element of Fin (PFuncs (V,C)); :: thesis: for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )
let a be set ; :: thesis: ( a in A ^ B implies ex c being set st
( c in B & c c= a ) )
assume a in A ^ B ; :: thesis: ex c being set st
( c in B & c c= a )
then consider b, c being set such that
b in A and
A1: c in B and
A2: a = b \/ c by Th15;
take c ; :: thesis: ( c in B & c c= a )
thus c in B by A1; :: thesis: c c= a
thus c c= a by A2, XBOOLE_1:7; :: thesis: verum