let V, C be set ; :: thesis: for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
A ^ D c= B ^ D
let A, B, D be Element of Fin (PFuncs (V,C)); :: thesis: ( A c= B implies A ^ D c= B ^ D )
deffunc H₁( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = $1 \/ $2;
defpred S₁[ Function, Function] means ( $1 in A & $2 in D & $1 tolerates $2 );
defpred S₂[ Function, Function] means ( $1 in B & $2 in D & $1 tolerates $2 );
set X1 = { H₁(s,t) where s, t is Element of PFuncs (V,C) : S₁[s,t] } ;
set X2 = { H₁(s,t) where s, t is Element of PFuncs (V,C) : S₂[s,t] } ;
assume A c= B ; :: thesis: A ^ D c= B ^ D
then A1: for s, t being Element of PFuncs (V,C) st S₁[s,t] holds
S₂[s,t] ;
{ H₁(s,t) where s, t is Element of PFuncs (V,C) : S₁[s,t] } c= { H₁(s,t) where s, t is Element of PFuncs (V,C) : S₂[s,t] } from FRAENKEL:sch 2(A1);
hence A ^ D c= B ^ D ; :: thesis: verum