let V, C be set ; :: thesis: for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
D ^ A c= D ^ B
let A, B, D be Element of Fin (PFuncs (V,C)); :: thesis: ( A c= B implies D ^ A c= D ^ B )
( D ^ A = A ^ D & D ^ B = B ^ D ) by Th3;
hence ( A c= B implies D ^ A c= D ^ B ) by Th14; :: thesis: verum