let A be set ; :: thesis: for X being non empty set
for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion B,f
let X be non empty set ; :: thesis: for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion B,f
let f be Function of X,[:(Fin A),(Fin A):]; :: thesis: for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion B,f
let B be Element of Fin X; :: thesis: for x being Element of X st x in B holds
f . x c= FinPairUnion B,f
let x be Element of X; :: thesis: ( x in B implies f . x c= FinPairUnion B,f )
assume A1: x in B ; :: thesis: f . x c= FinPairUnion B,f
then (FinPairUnion A) $$ B,f = (FinPairUnion A) $$ (B \/ {.x.}),f by ZFMISC_1:46
.= (FinPairUnion A) . ((FinPairUnion A) $$ B,f),(f . x) by A1, SETWISEO:29
.= ((FinPairUnion A) $$ B,f) \/ (f . x) by Def6 ;
hence f . x c= FinPairUnion B,f by Th26; :: thesis: verum