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 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.}]
proof
let B be Element of Fin X; :: thesis: for i being Element of X st S1[B] holds
S1[B \/ {.i.}]
let i be Element of X; :: thesis: ( S1[B] implies S1[B \/ {.i.}] )
assume FinUnion (B,f) = union (f .: B) ; :: thesis: S1[B \/ {.i.}]
hence FinUnion ((B \/ {.i.}),f) = (union (f .: B)) \/ (union {(f . i)}) by Th45
.= union ((f .: B) \/ {(f . i)}) by ZFMISC_1:78
.= union ((f .: B) \/ (Im (f,i))) by Th5
.= union (f .: (B \/ {i})) by RELAT_1:120 ;
:: thesis: verum
end;
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); :: thesis: verum