let A be set ; :: thesis: for X being non empty set

for B being Element of Fin X

for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds

FinPairUnion (B,f) = FinPairUnion (B,g)

let X be non empty set ; :: thesis: for B being Element of Fin X

for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds

FinPairUnion (B,f) = FinPairUnion (B,g)

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

FinPairUnion (B,f) = FinPairUnion (B,g)

let f, g be Function of X,[:(Fin A),(Fin A):]; :: thesis: ( f | B = g | B implies FinPairUnion (B,f) = FinPairUnion (B,g) )

set J = FinPairUnion A;

A1: [({}. A),({}. A)] = the_unity_wrt (FinPairUnion A) by Th19;

assume A2: f | B = g | B ; :: thesis: FinPairUnion (B,f) = FinPairUnion (B,g)

for B being Element of Fin X

for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds

FinPairUnion (B,f) = FinPairUnion (B,g)

let X be non empty set ; :: thesis: for B being Element of Fin X

for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds

FinPairUnion (B,f) = FinPairUnion (B,g)

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

FinPairUnion (B,f) = FinPairUnion (B,g)

let f, g be Function of X,[:(Fin A),(Fin A):]; :: thesis: ( f | B = g | B implies FinPairUnion (B,f) = FinPairUnion (B,g) )

set J = FinPairUnion A;

A1: [({}. A),({}. A)] = the_unity_wrt (FinPairUnion A) by Th19;

assume A2: f | B = g | B ; :: thesis: FinPairUnion (B,f) = FinPairUnion (B,g)

now :: thesis: FinPairUnion (B,f) = FinPairUnion (B,g)end;

hence
FinPairUnion (B,f) = FinPairUnion (B,g)
; :: thesis: verumper cases
( B = {} or B <> {} )
;

end;

suppose A3:
B = {}
; :: thesis: FinPairUnion (B,f) = FinPairUnion (B,g)

hence FinPairUnion (B,f) =
(FinPairUnion A) $$ (({}. X),f)

.= [({}. A),({}. A)] by A1, Th18, SETWISEO:31

.= (FinPairUnion A) $$ (({}. X),g) by A1, Th18, SETWISEO:31

.= FinPairUnion (B,g) by A3 ;

:: thesis: verum

end;.= [({}. A),({}. A)] by A1, Th18, SETWISEO:31

.= (FinPairUnion A) $$ (({}. X),g) by A1, Th18, SETWISEO:31

.= FinPairUnion (B,g) by A3 ;

:: thesis: verum

suppose A4:
B <> {}
; :: thesis: FinPairUnion (B,f) = FinPairUnion (B,g)

f .: B = g .: B
by A2, RELAT_1:166;

hence FinPairUnion (B,f) = FinPairUnion (B,g) by A4, SETWISEO:26; :: thesis: verum

end;hence FinPairUnion (B,f) = FinPairUnion (B,g) by A4, SETWISEO:26; :: thesis: verum