:: MULTOP_1  semantic presentation begin  definitionlet "f" be   ($#m1_hidden :::"Function":::); let "a", "b", "c" be    ($#m1_hidden :::"set"::: )  ; func "f" :::".":::  "(" "a" "," "b" "," "c" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: MULTOP_1:def 1 (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  ($#k3_xtuple_0 :::"["::: ) "a" "," "b" "," "c" ($#k3_xtuple_0 :::"]"::: ) )); end; 








:: deftheorem    defines :::"."::: MULTOP_1:def 1 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "f"))  ($#k1_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k3_xtuple_0 :::"]"::: ) ))))); 
 





























definitionlet "A", "B", "C", "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) "," (Set (Const "C")) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set (Const "D")); let "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); let "b" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "B")); let "c" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")); :: original: :::"."::: redefine func "f" :::".":::  "(" "a" "," "b" "," "c" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" "D"; end; 
theorem :: MULTOP_1:1 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) )))  ")" )) "holds"  (Bool (Set (Var "f1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "f2")))))) ; 
 
theorem :: MULTOP_1:2 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "B"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k4_domain_1 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k4_domain_1 :::"]"::: ) )))))  ")" )) "holds"  (Bool (Set (Var "f1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "f2"))))) ; 
 
theorem :: MULTOP_1:3 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "B"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "f1"))  ($#k2_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k2_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ))))  ")" )) "holds"  (Bool (Set (Var "f1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "f2"))))) ; 
 definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; mode TriOp of "A" is   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) "A" "," "A" "," "A" ($#k3_zfmisc_1 :::":]"::: ) ) "," "A"; end; scheme  :: MULTOP_1:sch 1 FuncEx3D{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "," (Set F3 "("  ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set F4 "("  ")" ) "st"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) "holds"  (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k4_domain_1 :::"]"::: ) ))])))))
 provided
(Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F4 "("  ")" ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t"))])))))
 proof 


end; scheme  :: MULTOP_1:sch 2 TriOpEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )] } : 
(Bool  "ex" (Set (Var "o")) "being"   ($#m1_subset_1 :::"TriOp":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Set (Var "o"))  ($#k2_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )])))
 provided
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t"))])))
 proof 


end; scheme  :: MULTOP_1:sch 3 Lambda3D{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F5(   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" )) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F4 "("  ")" ) } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "," (Set F3 "("  ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set F4 "("  ")" ) "st"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k4_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k4_domain_1 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ))))))
 proof 


end; scheme  :: MULTOP_1:sch 4 TriOpLambda{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F5(   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" )) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F4 "("  ")" ) } : 
(Bool  "ex" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "," (Set F3 "("  ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set F4 "("  ")" ) "st"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) "holds"  (Bool (Set (Set (Var "o"))  ($#k2_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ))))))
 proof 


end; definitionlet "f" be   ($#m1_hidden :::"Function":::); let "a", "b", "c", "d" be    ($#m1_hidden :::"set"::: )  ; func "f" :::".":::  "(" "a" "," "b" "," "c" "," "d" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: MULTOP_1:def 2 (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_xtuple_0 :::"["::: ) "a" "," "b" "," "c" "," "d" ($#k6_xtuple_0 :::"]"::: ) )); end; 









:: deftheorem    defines :::"."::: MULTOP_1:def 2 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "f"))  ($#k3_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_xtuple_0 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k6_xtuple_0 :::"]"::: ) ))))); 
 definitionlet "A", "B", "C", "D", "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k4_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) "," (Set (Const "C")) "," (Set (Const "D")) ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set (Const "E")); let "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); let "b" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "B")); let "c" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")); let "d" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "D")); :: original: :::"."::: redefine func "f" :::".":::  "(" "a" "," "b" "," "c" "," "d" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" "E"; end; 
theorem :: MULTOP_1:4 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "S")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "S")) ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) ($#k6_xtuple_0 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) ($#k6_xtuple_0 :::"]"::: ) )))  ")" )) "holds"  (Bool (Set (Var "f1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "f2")))))) ; 
 
theorem :: MULTOP_1:5 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "B"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set (Set (Var "f1"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ))))))  ")" )) "holds"  (Bool (Set (Var "f1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "f2"))))) ; 
 
theorem :: MULTOP_1:6 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "B"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set (Set (Var "f1"))  ($#k4_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k4_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )))))  ")" )) "holds"  (Bool (Set (Var "f1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "f2"))))) ; 
 definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; mode QuaOp of "A" is   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k4_zfmisc_1 :::"[:"::: ) "A" "," "A" "," "A" "," "A" ($#k4_zfmisc_1 :::":]"::: ) ) "," "A"; end; scheme  :: MULTOP_1:sch 5 FuncEx4D{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F5() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k4_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "," (Set F3 "("  ")" ) "," (Set F4 "("  ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set F5 "("  ")" ) "st"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" )  (Bool  "for" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F4 "("  ")" ) "holds"  (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k5_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) ($#k5_domain_1 :::"]"::: ) ))]))))))
 provided
(Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" )  (Bool  "for" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F4 "("  ")" ) (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F5 "("  ")" ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) "," (Set (Var "t"))]))))))
 proof 


end; scheme  :: MULTOP_1:sch 6 QuaOpEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )] } : 
(Bool  "ex" (Set (Var "o")) "being"   ($#m1_subset_1 :::"QuaOp":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Set (Var "o"))  ($#k4_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )])))
 provided
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) "," (Set (Var "t"))])))
 proof 


end; scheme  :: MULTOP_1:sch 7 Lambda4D{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F5() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F6(   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F4 "("  ")" )) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F5 "("  ")" ) } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k4_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "," (Set F3 "("  ")" ) "," (Set F4 "("  ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set F5 "("  ")" ) "st"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" )  (Bool  "for" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F4 "("  ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k5_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) ($#k5_domain_1 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "s")) ")" )))))))
 proof 


end; scheme  :: MULTOP_1:sch 8 QuaOpLambda{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) ","    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "o")) "being"   ($#m1_subset_1 :::"QuaOp":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "o"))  ($#k4_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ))))
 proof 


end;