let S be non empty non void ManySortedSign ; 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; 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; ( 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"
; 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; 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); ex y being Element of Args (o,A) st F # y = t
set D = len (the_arity_of o);
defpred S1[ 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 S1[k,x]
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
S1[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)
then reconsider p = p as Element of Args (o,A) by A9, MSAFREE2:5;
set fp = F # p;
take
p
; F # p = t
reconsider E = the Sorts of B * (the_arity_of o) as V2() 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
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; verum