let F1, F2 be V211() 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 set st H in bool S holds
F1 . H = F2 . H

proof

let H be set ; :: thesis: ( H in bool S implies F1 . H = F2 . H )
assume A8: H in bool S ; :: thesis: F1 . H = F2 . H
reconsider H = H as Subset of S by A8;
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:18; :: thesis: verum