let X be non empty set ; :: thesis: 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 ; :: thesis: 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); :: thesis: for B being Element of Fin X holds FinUnion B,f = union (f .: B)
defpred S₁[ Element of Fin X] means FinUnion $1,f = union (f .: $1);
A1: S₁[ {}. X]

proof

thus FinUnion ({}. X),f = union {} by Th59, ZFMISC_1:2
.= union (f .: ({}. X)) by RELAT_1:149 ; :: thesis: verum

end;

A2: for B being Element of Fin X
for i being Element of X st S₁[B] holds
S₁[B \/ {.i.}]

proof

let B be Element of Fin X; :: thesis: for i being Element of X st S₁[B] holds
S₁[B \/ {.i.}]
let i be Element of X; :: thesis: ( S₁[B] implies S₁[B \/ {.i.}] )
assume FinUnion B,f = union (f .: B) ; :: thesis: S₁[B \/ {.i.}]
hence FinUnion (B \/ {.i.}),f = (union (f .: B)) \/ (f . i) by Th60
.= (union (f .: B)) \/ (union {(f . i)}) by ZFMISC_1:31
.= union ((f .: B) \/ {(f . i)}) by ZFMISC_1:96
.= union ((f .: B) \/ (Im f,i)) by Th13
.= union (f .: (B \/ {i})) by RELAT_1:153 ;
:: thesis: verum

end;

thus for B being Element of Fin X holds S₁[B] from SETWISEO:sch 4(A1, A2); :: thesis: verum