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 c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds

f . x c= c ) holds

FinPairUnion (B,f) c= c

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 c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds

f . x c= c ) holds

FinPairUnion (B,f) c= c

let f be Function of X,[:(Fin A),(Fin A):]; :: thesis: for B being Element of Fin X

for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds

f . x c= c ) holds

FinPairUnion (B,f) c= c

let B be Element of Fin X; :: thesis: for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds

f . x c= c ) holds

FinPairUnion (B,f) c= c

let c be Element of [:(Fin A),(Fin A):]; :: thesis: ( ( for x being Element of X st x in B holds

f . x c= c ) implies FinPairUnion (B,f) c= c )

defpred S_{1}[ Element of Fin X] means ( $1 c= B implies (FinPairUnion A) $$ ($1,f) c= c );

assume A1: for x being Element of X st x in B holds

f . x c= c ; :: thesis: FinPairUnion (B,f) c= c

_{1}[ {}. X]
_{1}[C]
from SETWISEO:sch 4(A6, A2);

hence FinPairUnion (B,f) c= c ; :: thesis: verum

for f being Function of X,[:(Fin A),(Fin A):]

for B being Element of Fin X

for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds

f . x c= c ) holds

FinPairUnion (B,f) c= c

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 c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds

f . x c= c ) holds

FinPairUnion (B,f) c= c

let f be Function of X,[:(Fin A),(Fin A):]; :: thesis: for B being Element of Fin X

for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds

f . x c= c ) holds

FinPairUnion (B,f) c= c

let B be Element of Fin X; :: thesis: for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds

f . x c= c ) holds

FinPairUnion (B,f) c= c

let c be Element of [:(Fin A),(Fin A):]; :: thesis: ( ( for x being Element of X st x in B holds

f . x c= c ) implies FinPairUnion (B,f) c= c )

defpred S

assume A1: for x being Element of X st x in B holds

f . x c= c ; :: thesis: FinPairUnion (B,f) c= c

A2: now :: thesis: for C being Element of Fin X

for b being Element of X st S_{1}[C] holds

S_{1}[C \/ {.b.}]

A6:
Sfor b being Element of X st S

S

let C be Element of Fin X; :: thesis: for b being Element of X st S_{1}[C] holds

S_{1}[C \/ {.b.}]

let b be Element of X; :: thesis: ( S_{1}[C] implies S_{1}[C \/ {.b.}] )

assume A3: S_{1}[C]
; :: thesis: S_{1}[C \/ {.b.}]

_{1}[C \/ {.b.}]
; :: thesis: verum

end;S

let b be Element of X; :: thesis: ( S

assume A3: S

now :: thesis: ( C \/ {b} c= B implies (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c )

hence
Sassume A4:
C \/ {b} c= B
; :: thesis: (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c

then {b} c= B by XBOOLE_1:11;

then b in B by ZFMISC_1:31;

then A5: f . b c= c by A1;

(FinPairUnion A) $$ ((C \/ {.b.}),f) = (FinPairUnion A) . (((FinPairUnion A) $$ (C,f)),(f . b)) by Th18, SETWISEO:32

.= ((FinPairUnion A) $$ (C,f)) \/ (f . b) by Def6 ;

hence (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c by A3, A4, A5, Th9, XBOOLE_1:11; :: thesis: verum

end;then {b} c= B by XBOOLE_1:11;

then b in B by ZFMISC_1:31;

then A5: f . b c= c by A1;

(FinPairUnion A) $$ ((C \/ {.b.}),f) = (FinPairUnion A) . (((FinPairUnion A) $$ (C,f)),(f . b)) by Th18, SETWISEO:32

.= ((FinPairUnion A) $$ (C,f)) \/ (f . b) by Def6 ;

hence (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c by A3, A4, A5, Th9, XBOOLE_1:11; :: thesis: verum

proof

for C being Element of Fin X holds S
assume
{}. X c= B
; :: thesis: (FinPairUnion A) $$ (({}. X),f) c= c

(FinPairUnion A) $$ (({}. X),f) = the_unity_wrt (FinPairUnion A) by Th18, SETWISEO:31;

hence (FinPairUnion A) $$ (({}. X),f) c= c by Th20; :: thesis: verum

end;(FinPairUnion A) $$ (({}. X),f) = the_unity_wrt (FinPairUnion A) by Th18, SETWISEO:31;

hence (FinPairUnion A) $$ (({}. X),f) c= c by Th20; :: thesis: verum

hence FinPairUnion (B,f) c= c ; :: thesis: verum