let p be Element of REAL 3; :: thesis: for f1, f2, f3 being PartFunc of (REAL 3),REAL holds curl f1,f2,f3,p = |[((partdiff f3,p,2) - (partdiff f2,p,3)),((partdiff f1,p,3) - (partdiff f3,p,1)),((partdiff f2,p,1) - (partdiff f1,p,2))]|
let f1, f2, f3 be PartFunc of (REAL 3),REAL ; :: thesis: curl f1,f2,f3,p = |[((partdiff f3,p,2) - (partdiff f2,p,3)),((partdiff f1,p,3) - (partdiff f3,p,1)),((partdiff f2,p,1) - (partdiff f1,p,2))]|
curl f1,f2,f3,p = (|[(((partdiff f3,p,2) - (partdiff f2,p,3)) * 1),(((partdiff f3,p,2) - (partdiff f2,p,3)) * 0 ),(((partdiff f3,p,2) - (partdiff f2,p,3)) * 0 )]| + (((partdiff f1,p,3) - (partdiff f3,p,1)) * |[0 ,1,0 ]|)) + (((partdiff f2,p,1) - (partdiff f1,p,2)) * |[0 ,0 ,1]|) by EUCLID_8:59
.= (|[((partdiff f3,p,2) - (partdiff f2,p,3)),0 ,0 ]| + |[(((partdiff f1,p,3) - (partdiff f3,p,1)) * 0 ),(((partdiff f1,p,3) - (partdiff f3,p,1)) * 1),(((partdiff f1,p,3) - (partdiff f3,p,1)) * 0 )]|) + (((partdiff f2,p,1) - (partdiff f1,p,2)) * |[0 ,0 ,1]|) by EUCLID_8:59
.= (|[((partdiff f3,p,2) - (partdiff f2,p,3)),0 ,0 ]| + |[0 ,((partdiff f1,p,3) - (partdiff f3,p,1)),0 ]|) + |[(((partdiff f2,p,1) - (partdiff f1,p,2)) * 0 ),(((partdiff f2,p,1) - (partdiff f1,p,2)) * 0 ),(((partdiff f2,p,1) - (partdiff f1,p,2)) * 1)]| by EUCLID_8:59
.= |[(((partdiff f3,p,2) - (partdiff f2,p,3)) + 0 ),(0 + ((partdiff f1,p,3) - (partdiff f3,p,1))),(0 + 0 )]| + |[0 ,0 ,((partdiff f2,p,1) - (partdiff f1,p,2))]| by Lm6
.= |[(((partdiff f3,p,2) - (partdiff f2,p,3)) + 0 ),(((partdiff f1,p,3) - (partdiff f3,p,1)) + 0 ),(0 + ((partdiff f2,p,1) - (partdiff f1,p,2)))]| by Lm6
.= |[((partdiff f3,p,2) - (partdiff f2,p,3)),((partdiff f1,p,3) - (partdiff f3,p,1)),((partdiff f2,p,1) - (partdiff f1,p,2))]| ;
hence curl f1,f2,f3,p = |[((partdiff f3,p,2) - (partdiff f2,p,3)),((partdiff f1,p,3) - (partdiff f3,p,1)),((partdiff f2,p,1) - (partdiff f1,p,2))]| ; :: thesis: verum