deffunc H₁( object ) -> object = F₄((($1 `1) `1),(($1 `1) `2),($1 `2));
consider f being Function such that
A1: dom f = [:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>():] and
A2: for x being object st x in [:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>():] holds
f . x = H<sub>1</sub>(x) from FUNCT_1:sch 3();
reconsider f = f as ManySortedSet of [:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>():] by A1, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: for i, j, k being set st i in F<sub>1</sub>() & j in F<sub>2</sub>() & k in F<sub>3</sub>() holds
f . (i,j,k) = F<sub>4</sub>(i,j,k)
let i, j, k be set ; :: thesis: ( i in F<sub>1</sub>() & j in F<sub>2</sub>() & k in F<sub>3</sub>() implies f . (i,j,k) = F<sub>4</sub>(i,j,k) )
A3: ( [[i,j],k] `2 = k & [i,j,k] = [[i,j],k] ) ;
A4: ([[i,j],k] `1) `2 = j ;
A5: ([[i,j],k] `1) `1 = i ;
assume ( i in F₁() & j in F₂() & k in F₃() ) ; :: thesis: f . (i,j,k) = F₄(i,j,k)
then A6: [i,j,k] in [:F₁(),F₂(),F₃():] by MCART_1:69;
thus f . (i,j,k) = f . [i,j,k] by MULTOP_1:def 1
.= F₄(i,j,k) by A2, A6, A5, A4, A3 ; :: thesis: verum