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:40

.= (FinPairUnion A) . (((FinPairUnion A) $$ (B,f)),(f . x)) by A1, SETWISEO:20

.= ((FinPairUnion A) $$ (B,f)) \/ (f . x) by Def6 ;

hence f . x c= FinPairUnion (B,f) by Th10; :: thesis: verum

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:40

.= (FinPairUnion A) . (((FinPairUnion A) $$ (B,f)),(f . x)) by A1, SETWISEO:20

.= ((FinPairUnion A) $$ (B,f)) \/ (f . x) by Def6 ;

hence f . x c= FinPairUnion (B,f) by Th10; :: thesis: verum