let X, Y be non empty set ; :: thesis: for F being BinOp of Y
for t1, t2 being Function of X,Y
for B being Element of Fin X st F is commutative & F is associative & F is having_a_unity & ( for x being Element of X st x in B holds
t1 . x = t2 . x ) holds
F $$ (B,t1) = F $$ (B,t2)
let F be BinOp of Y; :: thesis: for t1, t2 being Function of X,Y
for B being Element of Fin X st F is commutative & F is associative & F is having_a_unity & ( for x being Element of X st x in B holds
t1 . x = t2 . x ) holds
F $$ (B,t1) = F $$ (B,t2)
let t1, t2 be Function of X,Y; :: thesis: for B being Element of Fin X st F is commutative & F is associative & F is having_a_unity & ( for x being Element of X st x in B holds
t1 . x = t2 . x ) holds
F $$ (B,t1) = F $$ (B,t2)
let B be Element of Fin X; :: thesis: ( F is commutative & F is associative & F is having_a_unity & ( for x being Element of X st x in B holds
t1 . x = t2 . x ) implies F $$ (B,t1) = F $$ (B,t2) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: for x being Element of X st x in B holds
t1 . x = t2 . x ; :: thesis: F $$ (B,t1) = F $$ (B,t2)
A4: B is Subset of X by FINSUB_1:16;
A5: dom (t1 | B) = (dom t1) /\ B by RELAT_1:61
.= X /\ B by FUNCT_2:def 1
.= B by XBOOLE_1:28, A4 ;
A6: dom (t2 | B) = (dom t2) /\ B by RELAT_1:61
.= X /\ B by FUNCT_2:def 1
.= B by XBOOLE_1:28, A4 ;
t1 | B = t2 | B

proof

for x being object st x in dom (t1 | B) holds
(t1 | B) . x = (t2 | B) . x

proof

let x be object ; :: thesis: ( x in dom (t1 | B) implies (t1 | B) . x = (t2 | B) . x )
assume A7: x in dom (t1 | B) ; :: thesis: (t1 | B) . x = (t2 | B) . x
then reconsider x1 = x as Element of X ;
(t1 | B) . x = t1 . x1 by A7, FUNCT_1:47
.= t2 . x1 by A2, A7, A5
.= (t2 | B) . x by A7, A5, A6, FUNCT_1:47 ;
hence (t1 | B) . x = (t2 | B) . x ; :: thesis: verum

end;

hence t1 | B = t2 | B by A5, A6; :: thesis: verum

end;

hence F $$ (B,t1) = F $$ (B,t2) by A1, SETWOP_2:7; :: thesis: verum