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 )
assume A1: A c= B ; :: thesis: 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] } ;
A2: for s, t being Element of PFuncs V,C st S₁[s,t] holds
S₂[s,t] by A1;
{ 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(A2);
hence A ^ D c= B ^ D ; :: thesis: verum