let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is "onto" holds
for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
let A, B be non-empty MSAlgebra over S; :: thesis: for F being ManySortedFunction of A,B st F is "onto" holds
for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
let F be ManySortedFunction of A,B; :: thesis: ( F is "onto" implies for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x )
assume A1: F is "onto" ; :: thesis: for o being OperSymbol of S
for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
let o be OperSymbol of S; :: thesis: for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x
let t be Element of Args (o,B); :: thesis: ex y being Element of Args (o,A) st F # y = t
set D = len (the_arity_of o);
defpred S₁[ object , object ] means ex y1 being Element of the Sorts of A . ((the_arity_of o) /. $1) st
( (F . ((the_arity_of o) /. $1)) . y1 = t . $1 & $2 = y1 );
A2: for k being Element of NAT st k in Seg (len (the_arity_of o)) holds
ex x being object st S₁[k,x]

proof

let k be Element of NAT ; :: thesis: ( k in Seg (len (the_arity_of o)) implies ex x being object st S₁[k,x] )
assume k in Seg (len (the_arity_of o)) ; :: thesis: ex x being object st S₁[k,x]
then A3: k in dom (the_arity_of o) by FINSEQ_1:def 3;
set s = (the_arity_of o) /. k;
A4: t . k in the Sorts of B . ((the_arity_of o) /. k) by A3, MSUALG_6:2;
rng (F . ((the_arity_of o) /. k)) = the Sorts of B . ((the_arity_of o) /. k) by A1;
then consider y1 being object such that
A5: y1 in the Sorts of A . ((the_arity_of o) /. k) and
A6: (F . ((the_arity_of o) /. k)) . y1 = t . k by A4, FUNCT_2:11;
reconsider y2 = y1 as Element of the Sorts of A . ((the_arity_of o) /. k) by A5;
take y1 ; :: thesis: S₁[k,y1]
take y2 ; :: thesis: ( (F . ((the_arity_of o) /. k)) . y2 = t . k & y1 = y2 )
thus ( (F . ((the_arity_of o) /. k)) . y2 = t . k & y1 = y2 ) by A6; :: thesis: verum

end;

consider p being FinSequence such that
A7: dom p = Seg (len (the_arity_of o)) and
A8: for k being Element of NAT st k in Seg (len (the_arity_of o)) holds
S₁[k,p . k] from MSUALG_8:sch 1(A2);
A9: len p = len (the_arity_of o) by A7, FINSEQ_1:def 3;
for k being Nat st k in dom p holds
p . k in the Sorts of A . ((the_arity_of o) /. k)

proof

let k be Nat; :: thesis: ( k in dom p implies p . k in the Sorts of A . ((the_arity_of o) /. k) )
assume k in dom p ; :: thesis: p . k in the Sorts of A . ((the_arity_of o) /. k)
then ex y1 being Element of the Sorts of A . ((the_arity_of o) /. k) st
( (F . ((the_arity_of o) /. k)) . y1 = t . k & p . k = y1 ) by A7, A8;
hence p . k in the Sorts of A . ((the_arity_of o) /. k) ; :: thesis: verum

end;

then reconsider p = p as Element of Args (o,A) by A9, MSAFREE2:5;
set fp = F # p;
take p ; :: thesis: F # p = t
reconsider E = the Sorts of B * (the_arity_of o) as non-empty ManySortedSet of dom (the_arity_of o) ;
A10: Args (o,B) = product E by PRALG_2:3;
A11: Seg (len (the_arity_of o)) = dom (the_arity_of o) by FINSEQ_1:def 3
.= dom ( the Sorts of B * (the_arity_of o)) by PRALG_2:3
.= dom t by A10, CARD_3:9 ;
A12: for k being Nat st k in dom t holds
(F # p) . k = t . k

proof

let k be Nat; :: thesis: ( k in dom t implies (F # p) . k = t . k )
assume A13: k in dom t ; :: thesis: (F # p) . k = t . k
then ex y1 being Element of the Sorts of A . ((the_arity_of o) /. k) st
( (F . ((the_arity_of o) /. k)) . y1 = t . k & p . k = y1 ) by A11, A8;
hence (F # p) . k = t . k by A11, A7, A13, MSUALG_3:def 6; :: thesis: verum

end;

dom (F # p) = dom ( the Sorts of B * (the_arity_of o)) by A10, CARD_3:9
.= dom t by A10, CARD_3:9 ;
hence F # p = t by A12; :: thesis: verum