let F1, F2 be V211() Function of (bool S),(bool S); :: thesis: ( ( for G being Subset of S holds F1 . G = SigFaxTau f,G,R,BASSIGN ) & ( for G being Subset of S holds F2 . G = SigFaxTau f,G,R,BASSIGN ) implies F1 = F2 )
assume that
A6: for G being Subset of S holds F1 . G = SigFaxTau f,G,R,BASSIGN and
A7: for G being Subset of S holds F2 . G = SigFaxTau f,G,R,BASSIGN ; :: thesis: F1 = F2
for G being set st G in bool S holds
F1 . G = F2 . G

proof

let G be set ; :: thesis: ( G in bool S implies F1 . G = F2 . G )
assume A8: G in bool S ; :: thesis: F1 . G = F2 . G
reconsider G = G as Subset of S by A8;
F1 . G = SigFaxTau f,G,R,BASSIGN by A6
.= F2 . G by A7 ;
hence F1 . G = F2 . G ; :: thesis: verum

end;

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