let V, C be set ; :: thesis: for A, B being Element of Fin (PFuncs (V,C)) st ( for a being set st a in A holds
a in B ) holds
A c= B
let A, B be Element of Fin (PFuncs (V,C)); :: thesis: ( ( for a being set st a in A holds
a in B ) implies A c= B )
assume A1: for a being set st a in A holds
a in B ; :: thesis: A c= B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume x in A ; :: thesis: x in B
hence x in B by A1; :: thesis: verum