let T be non empty RelStr ; :: thesis: for A being Subset of T
for n being Element of NAT holds (Fcl (A ` ),n) ` = Fint A,n
let A be Subset of T; :: thesis: for n being Element of NAT holds (Fcl (A ` ),n) ` = Fint A,n
let n be Element of NAT ; :: thesis: (Fcl (A ` ),n) ` = Fint A,n
Fint A,n = ((Fint ((A ` ) ` ),n) ` ) `
.= (Fcl (A ` ),n) ` by Th27 ;
hence (Fcl (A ` ),n) ` = Fint A,n ; :: thesis: verum