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₁[ 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

A2: now

let C be Element of Fin X; :: thesis: for b being Element of X st S₁[C] holds
S₁[C \/ {.b.}]
let b be Element of X; :: thesis: ( S₁[C] implies S₁[C \/ {.b.}] )
assume A3: S₁[C] ; :: thesis: S₁[C \/ {.b.}]

now

assume 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:37;
then A5: f . b c= c by A1;
(FinPairUnion A) $$ (C \/ {.b.}),f = (FinPairUnion A) . ((FinPairUnion A) $$ C,f),(f . b) by Th37, SETWISEO:41
.= ((FinPairUnion A) $$ C,f) \/ (f . b) by Def6 ;
hence (FinPairUnion A) $$ (C \/ {.b.}),f c= c by A3, A4, A5, Th25, XBOOLE_1:11; :: thesis: verum

end;

hence S₁[C \/ {.b.}] ; :: thesis: verum

end;

A6: S₁[ {}. X]

proof

assume {}. X c= B ; :: thesis: (FinPairUnion A) $$ ({}. X),f c= c
(FinPairUnion A) $$ ({}. X),f = the_unity_wrt (FinPairUnion A) by Th37, SETWISEO:40;
hence (FinPairUnion A) $$ ({}. X),f c= c by Th39; :: thesis: verum

end;

for C being Element of Fin X holds S₁[C] from SETWISEO:sch 4(A6, A2);
hence FinPairUnion B,f c= c ; :: thesis: verum