:: deftheorem defines curl PDIFF_4:def 10 :
for f1, f2, f3 being PartFunc of (REAL 3),REAL
for p being Element of REAL 3 holds curl (f1,f2,f3,p) = ((((partdiff (f3,p,2)) - (partdiff (f2,p,3))) * <e1>) + (((partdiff (f1,p,3)) - (partdiff (f3,p,1))) * <e2>)) + (((partdiff (f2,p,1)) - (partdiff (f1,p,2))) * <e3>);