let X be non empty set ; for A being set
for f being Function of X,(Fin A)
for B being Element of Fin X holds FinUnion (B,f) = union (f .: B)
let A be set ; for f being Function of X,(Fin A)
for B being Element of Fin X holds FinUnion (B,f) = union (f .: B)
let f be Function of X,(Fin A); for B being Element of Fin X holds FinUnion (B,f) = union (f .: B)
defpred S1[ Element of Fin X] means FinUnion ($1,f) = union (f .: $1);
A1:
for B being Element of Fin X
for i being Element of X st S1[B] holds
S1[B \/ {.i.}]
FinUnion (({}. X),f) = union (f .: ({}. X))
by Th44, ZFMISC_1:2;
then A2:
S1[ {}. X]
;
thus
for B being Element of Fin X holds S1[B]
from SETWISEO:sch 4(A2, A1); verum