let F1, F2 be c=-monotone Function of (bool S),(bool S); :: thesis: ( ( for H being Subset of S holds F1 . H = SigFoaxTau (g,f,H,R,BASSIGN) ) & ( for H being Subset of S holds F2 . H = SigFoaxTau (g,f,H,R,BASSIGN) ) implies F1 = F2 )
assume that
A6: for H being Subset of S holds F1 . H = SigFoaxTau (g,f,H,R,BASSIGN) and
A7: for H being Subset of S holds F2 . H = SigFoaxTau (g,f,H,R,BASSIGN) ; :: thesis: F1 = F2
for H being object st H in bool S holds
F1 . H = F2 . H

proof

let H be object ; :: thesis: ( H in bool S implies F1 . H = F2 . H )
assume H in bool S ; :: thesis: F1 . H = F2 . H
then reconsider H = H as Subset of S ;
F1 . H = SigFoaxTau (g,f,H,R,BASSIGN) by A6
.= F2 . H by A7 ;
hence F1 . H = F2 . H ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:12; :: thesis: verum