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)

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

per cases ( B = {} or B <> {} ) ;

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;

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;

end;

end;

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