consider Bo being Subset of B, yo being Function of Bo,A such that
A1: ( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } ) by LM1;
thus ex b₁ being finite Subset of B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } & b₁ = Bo ) by A1; :: thesis: verum